search

Z3Prover / z3

The Z3 Theorem Prover
Other
9.96k stars 1.46k forks source link

Incorrect definition order in `get-model` #7268

Open yav opened 6 days ago

yav commented 6 days ago

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.