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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9cb3387c8cd763f5d112a1657a568dd6bc5f7636..9453adefd9f0fb588c3c3044a8502ba452feeb01 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2057,10 +2057,6 @@ void SmtEngine::setDefaults() {
     }
   }
   if( options::dtStcInduction() ){
-    //leads to unfairness FIXME
-    if( !options::dtForceAssignment.wasSetByUser() ){
-      options::dtForceAssignment.set( true );
-    }
     //try to remove ITEs from quantified formulas
     if( !options::iteDtTesterSplitQuant.wasSetByUser() ){
       options::iteDtTesterSplitQuant.set( true );

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index e8149316ccef04c2cb3b6e3709e5550b91a90c9b..af242b4089f09371ed5e13022319c0b17de31fc8 100644 (file)
--- 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 (file)
index 0000000..d3e54e0
--- /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)
+