Outermost existential quantifier prevents solution from being found

[pclayton]

If all occurrences of a variable in a set of asserted formulas are existentially quantified, I don't think this change makes satisfiability of the formulas any harder. I tried a few examples to confirm that introducing such an exists preserves satisfiability but quickly found an example where this causes the result to change from sat to unknown.

For example

(get-info :version)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(assert (> a 0))
(assert (> b 0))
(assert (= (* c c) (+ (* a a) (* b b))))
(check-sat)

produces

(:version "4.12.2")
sat

as expected. However, existentially quantifying over c as follows:

(get-info :version)
(declare-const a Int)
(declare-const b Int)
(assert (> a 0))
(assert (> b 0))
(assert (exists ((c Int)) (= (* c c) (+ (* a a) (* b b)))))
(check-sat)
(get-info :reason-unknown)

produces

(:version "4.12.2")
unknown
(:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))")

Is the above behavior expected? For the above examples, we get sat in both cases if, say, (* b b) is replaced by b. Is there any way to predict when unknown would (likely) occur by such introduction of an existential quantifier?

[LeventErkok]

Existentials and non-linear arithmetic together can throw the solver off. Try:

(check-sat-using (then purify-arith nra))

you'll see that z3 will produce sat with this tactic in your second example too.

[pclayton]

Thank you for drawing my attention to the use of tactics. For the benefit of others, was able to test the effect of a tactic with (apply <tactic>), e.g.

(apply purify-arith)

[NikolajBjorner]

For the existential formula, by default it uses the AUFLIA tactic, which invokes the arithmetic solver that is highly incomplete with quantifiers.
You can set smt.auto_config=false and smt.arith.solver=6 or use tactics as described above. When arith.solver=6 is fully tuned it will become default for also AUFLIA.

[pclayton]

Thank you, it is useful to know about this tuning.