Z3 gives different answer depending on the value of fixedpoint.xform.inline_eager

[GuerricChupin]

I have the following code (if you are interested in why it exists, please read my StackOverflow question).

I use Z3 4.5.1 compiled from the master branch (and recompiled something like an hour ago) with g++ 6.3.0 on Ubuntu 17.04.

When calling z3 -smt2 so.smt2, I get:

sat
(and (Main!slice!1 false) (not (>= (:var 5) 0)) (Main!slice!1 true))

However if I call z3 -smt2 so.smt2 fixedpoint.xform.inline_eager=false, I get:

unsat
(define-fun Init ((x!0 Int)) Bool
  (>= x!0 10))
(define-fun Main ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
  (and x!2 (>= x!1 1)))
(define-fun Trans ((x!0 Int)
 (x!1 Int)
 (x!2 Bool)
 (x!3 Int)
 (x!4 Int)
 (x!5 Bool)) Bool
  (and (or (>= x!4 1) (not x!5)) (= x!5 (>= x!1 0))))

I think the second answer is the correct one. Regardless, I doubt that this parameter should change the result so drastically.

[agurfinkel]

Seems to be an interaction between slice and inline transformations. The option fixedpoint.xform.slice=false also gives a correct result independently of the inline setting. You can turn slicing off as a workaround for now.