Bad parsing of z3 counterexamples output
The source corresponding is jlamp_projections.mlw. The debug flag cntex_collection does not work on this.
The problem seems to be with to_int1!395 in the output ?
(define-fun to_int1!395 ((x!0 byte)) Int
(ite (= x!0 byte!val!1) 1
127))
(define-fun k!382 ((x!0 byte)) byte
(ite (= x!0 byte!val!1) byte!val!1
byte!val!0))
(define-fun to_int1 ((x!0 byte)) Int
(to_int1!395 (k!382 x!0)))