Quantifier instantion not happening - pattern bug?


Given the program below, Z3 4.3.2 and 4.4.0 55ca6ce44b2f (both Win x64) immediately report unknown, despite the fact that the given terms and patterns should allow it to instantiate each forall once, thereby showing that the goal is unsat.
(set-option :auto_config false) ; IMPORTANT
(set-option :smt.mbqi false)    ; IMPORTANT
(set-option :smt.qi.profile true)

(declare-fun fun (Int) Int)
(declare-fun funLim (Int) Int)

(declare-const x Int)

(assert (forall ((x Int)) (!
  (= (fun x) (+ 1 (funLim x)))
  :pattern ((fun x)))))

(assert (forall ((x Int)) (!
  (= (fun x) (funLim x))
  :pattern ((fun x)))))
(assert (not ; goal
  (= (fun x) (+ 1 (fun x))))) ; Change second fun to funLim and Z3 reports unsat
(check-sat) ; unknown
(get-info :all-statistics) ; no forall instantiated (if funLim is used, both are instantiated once)
Am I missing something here that would explain why Z3 doesn't perform the instantiation, or is this a bug in the triggering code?



wintersteiger wrote Mar 20, 2015 at 3:18 PM

There is something wrong with the simplifier, because (fun x) != (fun x) + 1 is lost somewhere along the line. Until that is fixed, you can enable the macro finder which will get you the desired behavior quickly:
(set-option :smt.macro_finder true)

mschwerhoff wrote Mar 24, 2015 at 10:47 AM

Thanks for looking into this! I activated the macro finder, but it significantly slowed down our test suite (~2.5x), and worse, it made 5 tests fail. If you are interested, I could look into the failing examples and try to distill minimal versions.

mschwerhoff wrote Apr 22, 2015 at 11:28 AM

FYI: The problem still exists in Z3 4.4.0 9bff93279f75 x64 (a nightly build I got from GitHub/bin)

mschwerhoff wrote May 8, 2015 at 6:54 AM

FYI: The problem still exists in the official Z3 4.4.0 release (https://github.com/Z3Prover/bin/blob/master/releases/z3-4.4.0-x64-win.zip)

wintersteiger wrote May 19, 2015 at 10:56 AM

Migrated to the new issue tracker on github.com, see here.

The z3 website on codeplex is being retired, from now on please use the issue tracker on github.