Closed alberdingk-thijm closed 4 years ago
This is possibly related to #31, although it's a different symptom. It looks like a problem with the unboxed encoding not properly encoding tuple comparisons. I came up with the following minimal example (only the last few lines are relevant):
type attribute = bool
let nodes = 1
let edges = {}
let trans e x = x
let merge n x y = x
let assert n x = x
symbolic foo : bool
let init n =
(if foo then (1,2) else (3,4)) =
(if foo then (1,2) else (3,4))
The symbolic variable and if statement are just there so we can't statically do the comparison during partial evaluation.
Managed to trigger an interesting error with a more complicated
assert
function that I was testing for partitioning. I'll see about coming up with a minimal working example, but here is the complete code.The error appears to be triggered by the
assert
function. The stack trace is (usingmaster
):This points to something going wrong when calling
lift2
withinencode_exp_z3_assert
.