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/ext-ex-deq-trigger.smt2 | |
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/ext-ex-deq-trigger.smt2')
-rw-r--r-- | test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 | 26 |
1 files changed, 26 insertions, 0 deletions
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) + |