You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Here's an odd bug that seems to occur when flattening and then encoding certain examples.
The below code leads to an assertion failure during execution of SmtUnboxed.encode_exp_z3_single:
typeattribute = bool
symbolic failed : option[(int,int)]
letedge_to_int_paire=match e with|0~1 -> (0, 1)
|1~0 -> (1, 0)
let nodes =2let edges = {0=1;}
letinitn= n =0nlettransex=!(Some (edge_to_int_pair e) = failed) && x
letmergenxy= x || y
let sol = solution { init = init; trans = trans; merge = merge; }
assert foldNodes (funuvacc -> acc && v) sol true
The source of the error seems to be that encode_exp_z3_single is given an expression ! ((true,0u32,1u32) = (symbolic-failed-proj-0~76,symbolic-failed-proj-1~77,symbolic-failed-proj-2~78)) && x~68, which it can't handle. Note that the tuple comparison in this expression should have been flattened into component comparisons, but for whatever reason, that has not happened here.
The error does not occur when the trans function is written out as:
lettransex=let pair = edge_to_int_pair e in!(Some pair = failed) && x
The text was updated successfully, but these errors were encountered:
Here's an odd bug that seems to occur when flattening and then encoding certain examples.
The below code leads to an assertion failure during execution of
SmtUnboxed.encode_exp_z3_single
:The source of the error seems to be that
encode_exp_z3_single
is given an expression! ((true,0u32,1u32) = (symbolic-failed-proj-0~76,symbolic-failed-proj-1~77,symbolic-failed-proj-2~78)) && x~68
, which it can't handle. Note that the tuple comparison in this expression should have been flattened into component comparisons, but for whatever reason, that has not happened here.The error does not occur when the trans function is written out as:
The text was updated successfully, but these errors were encountered: