diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-10 14:35:25 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-10 14:35:37 +0100 |
| commit | 81dca680f6c88d10b56a0ed065d470d907766e21 (patch) | |
| tree | 4410fa473ecb6848f7976b2b6a00188ac5e44775 /test/regress/regress0/quantifiers | |
| parent | 50c8533760bfd5b1f803d52bc4318c544521e6af (diff) | |
Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
Diffstat (limited to 'test/regress/regress0/quantifiers')
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 4 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 | 26 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/matching-lia-1arg.smt2 | 8 |
3 files changed, 37 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index e6b0a59fc..939b0d22c 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -61,7 +61,9 @@ TESTS = \ mix-simp.smt2 \ mix-coeff.smt2 \ mix-match.smt2 \ - ari056.smt2 + ari056.smt2 \ + ext-ex-deq-trigger.smt2 \ + matching-lia-1arg.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 b/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 new file mode 100644 index 000000000..f6f96fe02 --- /dev/null +++ b/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --relational-triggers +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-sort U 0) + +(declare-const k U) +(declare-const ff U) +(declare-const ffk U) +(declare-fun fun1 (Int) Int) +(declare-fun fun2 (Int) Int) +(declare-fun c (U U) U) +(declare-fun app (U Int) Int) + +(assert (forall ((f U) (g U)) (=> (forall ((x Int)) (= (app f x) (app g x))) (= f g)) )) + +(assert (forall ((x Int)) (= (app ff x) (+ (fun1 x) (fun2 x))))) +(assert (forall ((x Int)) (= (app ffk x) (+ (fun1 (app k x)) (fun2 (app k x)))))) + +(assert (forall ((f U) (g U) (x Int)) (= (app (c f g) x) (app f (app g x))))) + +(assert (not (= (c ff k) ffk))) + +(check-sat) + diff --git a/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 b/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 new file mode 100644 index 000000000..aaf9b2c1f --- /dev/null +++ b/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --purify-triggers +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(declare-fun P (Int) Bool) +(assert (forall ((x Int)) (P (* 2 x)))) +(assert (not (P 38))) +(check-sat) + |