Add benchmark requiring subgoal generation with induction. Disable option. (#1806)

1 files changed, 66 insertions, 0 deletions

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)
+