diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-07 14:43:34 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-07 21:43:34 +0100 |
| commit | c94d59516c62b481c7984830cf26753af16100a8 (patch) | |
| tree | c1206aecd9fc3b6e53799080c6f6feca295c24fa /test/regress/regress0/quantifiers | |
| parent | 5cc5bc2eafa90c763e727868c6149b5c370e63f7 (diff) | |
Fix issue with free variables introduced by quantifier rewriter (#5602)
This was caused by the quantifiers rewriting eliminating extended arithmetic operators, which was required due to the way counterexample-guided quantifier instantiation used to work with preprocessing. The technique is now more robust and this option can be deleted.
This fixes a debug assertion failure from UFNIA SMT-LIB, a minimized benchmark is included as a regression.
Diffstat (limited to 'test/regress/regress0/quantifiers')
| -rw-r--r-- | test/regress/regress0/quantifiers/ufnia-fv-delta.smt2 | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/ufnia-fv-delta.smt2 b/test/regress/regress0/quantifiers/ufnia-fv-delta.smt2 new file mode 100644 index 000000000..dfb87a1b9 --- /dev/null +++ b/test/regress/regress0/quantifiers/ufnia-fv-delta.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat +(set-logic UFNIA) +(assert (exists ((k Int)) (not (=> (forall ((a Int) (b Int)) (! (= k (ite (= 0 (mod a 2)) 1 0)) :pattern (b))) false)))) +(check-sat) |