diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-25 11:02:24 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-25 11:02:24 -0500 |
commit | a24e6ed96031e7ac3978201ed80fb771ee0f425e (patch) | |
tree | d5cb4f56d35a329c74079361acf53e4f9f3c4dff /test | |
parent | dbc501933c7e77fc61dcf6092050d3bb67ba5a49 (diff) |
Add benchmark requiring subgoal generation with induction. Disable option. (#1806)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/isaplanner-goal20.smt2 | 66 |
2 files changed, 67 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index e8149316c..af242b408 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1242,6 +1242,7 @@ REG1_TESTS = \ regress1/quantifiers/inst-max-level-segf.smt2 \ regress1/quantifiers/inst-prop-simp.smt2 \ regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 \ + regress1/quantifiers/isaplanner-goal20.smt2 \ regress1/quantifiers/is-even.smt2 \ regress1/quantifiers/javafe.ast.StmtVec.009.smt2 \ regress1/quantifiers/mix-coeff.smt2 \ diff --git a/test/regress/regress1/quantifiers/isaplanner-goal20.smt2 b/test/regress/regress1/quantifiers/isaplanner-goal20.smt2 new file mode 100644 index 000000000..d3e54e0af --- /dev/null +++ b/test/regress/regress1/quantifiers/isaplanner-goal20.smt2 @@ -0,0 +1,66 @@ +; COMMAND-LINE: --quant-ind --conjecture-gen +; EXPECT: unsat +(set-logic UFDTLIA) +(set-info :status unsat) +(declare-datatypes ((Nat 0)) (((succ (pred Nat)) (zero)) +)) +(declare-datatypes ((Lst 0)) (((cons (head Nat) (tail Lst)) (nil)) +)) +(declare-datatypes ((Tree 0)) (((node (data Nat) (left Tree) (right Tree)) (leaf)) +)) +(declare-datatypes ((Pair 0)(ZLst 0)) (((mkpair (first Nat) (second Nat))) +((zcons (zhead Pair) (ztail ZLst)) (znil)) +)) +(declare-fun P (Nat) Bool) +(declare-fun f (Nat) Nat) +(declare-fun less (Nat Nat) Bool) +(declare-fun plus (Nat Nat) Nat) +(declare-fun minus (Nat Nat) Nat) +(declare-fun mult (Nat Nat) Nat) +(declare-fun nmax (Nat Nat) Nat) +(declare-fun nmin (Nat Nat) Nat) +(declare-fun nat-to-int (Nat) Int) +(declare-fun append (Lst Lst) Lst) +(declare-fun len (Lst) Nat) +(declare-fun drop (Nat Lst) Lst) +(declare-fun take (Nat Lst) Lst) +(declare-fun count (Nat Lst) Nat) +(declare-fun last (Lst) Nat) +(declare-fun butlast (Lst) Lst) +(declare-fun mem (Nat Lst) Bool) +(declare-fun delete (Nat Lst) Lst) +(declare-fun rev (Lst) Lst) +(declare-fun lmap (Lst) Lst) +(declare-fun filter (Lst) Lst) +(declare-fun dropWhile (Lst) Lst) +(declare-fun takeWhile (Lst) Lst) +(declare-fun ins1 (Nat Lst) Lst) +(declare-fun insort (Nat Lst) Lst) +(declare-fun sorted (Lst) Bool) +(declare-fun sort (Lst) Lst) +(declare-fun zip (Lst Lst) ZLst) +(declare-fun zappend (ZLst ZLst) ZLst) +(declare-fun zdrop (Nat ZLst) ZLst) +(declare-fun ztake (Nat ZLst) ZLst) +(declare-fun zrev (ZLst) ZLst) +(declare-fun mirror (Tree) Tree) +(declare-fun height (Tree) Nat) +(define-fun leq ((x Nat) (y Nat)) Bool (or (= x y) (less x y))) +(assert (forall ((x Nat)) (>= (nat-to-int x) 0) )) +(assert (forall ((x Nat) (y Nat)) (=> (= (nat-to-int x) (nat-to-int y)) (= x y)) )) +(assert (= (nat-to-int zero) 0)) +(assert (forall ((x Nat)) (= (nat-to-int (succ x)) (+ 1 (nat-to-int x))) )) +(assert (forall ((x Nat)) (= (less x zero) false) )) +(assert (forall ((x Nat)) (= (less zero (succ x)) true) )) +(assert (forall ((x Nat) (y Nat)) (= (less (succ x) (succ y)) (less x y)) )) +(assert (forall ((x Nat) (y Nat)) (= (less x y) (< (nat-to-int x) (nat-to-int y))) )) +(assert (= (len nil) zero)) +(assert (forall ((x Nat) (y Lst)) (= (len (cons x y)) (succ (len y))) )) +(assert (forall ((i Nat)) (= (insort i nil) (cons i nil)) )) +(assert (forall ((i Nat) (x Nat) (y Lst)) (= (insort i (cons x y)) (ite (less i x) (cons i (cons x y)) (cons x (insort i y)))) )) +(assert (= (sort nil) nil)) +(assert (forall ((x Nat) (y Lst)) (= (sort (cons x y)) (insort x (sort y))) )) +(assert (not (forall ((l Lst)) (= (len (sort l)) (len l)) ))) +(check-sat) +(exit) + |