1

Consider the following SMTLIB program (on rise4fun here):

(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.arith.nl.gb false)

(declare-const n Int)
(declare-const i Int)
(declare-const r Int)

(assert (= i n))
(assert (= r (* i n)))

(push)
(assert (not (= r (* n n))))
(check-sat) ; unknown
(pop)

Although it appears to only require reasoning with syntactic equality, Z3 (4.3.2 official release, and also 4.4.0 b6c40c6c0eaf) nevertheless fails to show that the final assertion is unsat.

Unexpectedly (at least for me), setting smt.arith.nl.gb to true makes the example verify (i.e. the check-sat yields unsat).

For what it's worth, here are some further observations:

  • The final assertion can be shown unsat if the multiplication is changed to (* i n) or (* n i), respectively

  • It cannot be shown unsat if the multiplication is changed to (* i i)

  • (push) and (pop) don't appear to affect the example, i.e. they can be removed without affecting the described observations

Is this a bug or is there a reason that smt.arith.nl.gb is required to show this example unsat?

Malte Schwerhoff
  • 12,684
  • 4
  • 41
  • 71

1 Answers1

2

This is not necessarily a bug. The Groebner-basis computation solves the problem, so the unsat result is found quickly (it's good, so it's enabled by default). Further, disabling auto_config also means that a host of other options is not set up depending on the problem (but it doesn't make a difference in this particular case).

Note that some tactics, solvers, or simplifiers will simply give up when they see a multiplication expression, irregardless of whether the problem happens to be easy to solve for humans or other solvers. In this particular case, the non-linear solver gives up after smt.arith.nl.rounds is exhausted (1024 by default), so it returns unknown.

One of the tactics that solves this problem quickly is solve-eqs, but this is not part of the default tactic (in this case it runs the qfnia tactic). If it pays off on your problems, you can add that easily by replacing the check-sat command with

(check-sat-using (then solve-eqs qfnia))

whether this should be the default is debatable and up to benchmarking, but it isn't really a bug.

Another tactic that solves this problem quickly is the NLSAT solver, e.g., 

(check-sat-using nlsat)
Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30