Closed
Description
This is with version 4.13.0
The result of get-model sometimes contains definitions that are out of order, so you can't give them back to z3. Here is an example of an answer I am getting:
...
(define-fun mk_arc_483
((x!0 (Array (_ BitVec 32) (_ BitVec 32))) (x!1 (_ BitVec 32))
(x!2 (_ BitVec 32)))
tree_arc_486
(ite (and (= x!0 (_ as-array k!295)) (= x!1 #x0000a261) (= x!2 #x0000a261))
Arc_End_527 (Arc_Step_528 #x00000000 Arc_End_527)))
(define-fun k!295 ((x!0 (_ BitVec 32))) (_ BitVec 32) #x00000000))
Note that mk_arc_483 uses k!295, but k!295 is defined after it.
Metadata
Assignees
Labels
No labels