Z3 4.0 Additional output in the model

Question

When I try to get the model string along with the variables that I define, I get additional output in the model as -

z3name!0=3, z3name!1=-2, z3name!10=0, z3name!11=0, z3name!12=0, z3name!13=0, z3name!14=0, z3name!15=0, z3name!2=0, z3name!3=0, z3name!4=2, z3name!5=2, z3name!6=0, z3name!7=-3, z3name!8=2, z3name!9=0 

I want to know what is the erroneous conclusion? Or are these some intermediate variables that are used by Z3?

Because the values ​​for the variables that I defined suit me. I had not seen such an exit before, so I had such a doubt.

Answer 1

Z3 has several preprocessing steps. Some of them introduce new variables. New variables are usually removed from the resulting model. If it is not, this is a mistake. However, this error does not affect the correctness. This is just a nuisance.

It would be great if you could post your issue. We could determine which preprocessing step does not eliminate the input helper variables.

Answer 2

I understand that this is an old topic, but I found that I have the same “mistake” as Leonardo called it. Since the OP did not post its code, I thought mine could help fix it (although this additional output is not a problem for me as long as the validity is really preserved).

It seems that if I change the "/" in the last statement, for example, "+", the problem disappears.

 (declare-fun fun0!0 () Int) (declare-fun fun0!-1 () Int) (declare-fun var0 () Int) (assert (and (and (or (= fun0!0 0) (= fun0!0 1) (= fun0!0 2)) (or (= fun0!-1 0) (= fun0!-1 1) (= fun0!-1 2)) (or (= var0 1) (= var0 -1)) ) (and (or (= var0 0) (= var0 -1))) )) (define-fun fun0 ((i! Int)) Int (ite (= i! 0) fun0!0 (ite (= i! -1) fun0!-1 (- 0 1) ) ) ) (assert (= (fun0 var0) (/ var0 var0) )) (check-sat)