Increasing coverage (#2683)

This PR adds/revises tests in order to increase coverage in some preprocessing passes and in proofs done with --fewer-preprocessing-holes flag.

8 files changed, 64 insertions, 2 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5aea954e3..0313f0b13 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -157,6 +157,8 @@ set(regress_0_tests
   regress0/buggy-ite.smt2
   regress0/bv/ackermann1.smt2
   regress0/bv/ackermann2.smt2
+  regress0/bv/ackermann3.smt2
+  regress0/bv/ackermann4.smt2
   regress0/bv/bool-to-bv.smt2
   regress0/bv/bug260a.smt
   regress0/bv/bug260b.smt
@@ -171,7 +173,8 @@ set(regress_0_tests
   regress0/bv/bv-options2.smt2
   regress0/bv/bv-options3.smt2
   regress0/bv/bv-options4.smt2
-  regress0/bv/bv-to-bool.smt
+  regress0/bv/bv-to-bool1.smt
+  regress0/bv/bv-to-bool2.smt2
   regress0/bv/bv2nat-ground-c.smt2
   regress0/bv/bv2nat-simp-range.smt2
   regress0/bv/bvmul-pow2-only.smt2
diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2
index 4d2e828b5..30c87333e 100644
--- a/test/regress/regress0/bug217.smt2
+++ b/test/regress/regress0/bug217.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --fewer-preprocessing-holes
 ; EXPECT: unsat
 (set-logic QF_UF)
 (set-info :status unsat)
diff --git a/test/regress/regress0/bv/ackermann3.smt2 b/test/regress/regress0/bv/ackermann3.smt2
new file mode 100644
index 000000000..8e47c8840
--- /dev/null
+++ b/test/regress/regress0/bv/ackermann3.smt2
@@ -0,0 +1,23 @@
+; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic QF_ABV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+
+(define-sort bv () (_ BitVec 4))
+(define-sort abv () (Array bv bv))
+
+(declare-fun v0 () (_ BitVec 4))
+(declare-fun v1 () (_ BitVec 4))
+(declare-fun a () abv)
+(declare-fun b () abv)
+(declare-fun c () abv)
+
+(assert (not (= (select a (select b (select c v0))) (select a (select b (select c v1))))))
+
+(assert (= v0 v1))
+
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/ackermann4.smt2 b/test/regress/regress0/bv/ackermann4.smt2
new file mode 100644
index 000000000..cb8ad2e55
--- /dev/null
+++ b/test/regress/regress0/bv/ackermann4.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_UFBV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v0 () (_ BitVec 4))
+(declare-fun f ((_ BitVec 4)) (_ BitVec 4))
+(declare-fun g ((_ BitVec 4)) (_ BitVec 4))
+
+(assert (= (f v0) (g (f v0))))
+(assert (= (f (f v0)) (g (f v0))))
+(assert (= (f (f (f v0))) (g (f v0))))
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/bool-to-bv.smt2 b/test/regress/regress0/bv/bool-to-bv.smt2
index 92c7e4117..8706c51a8 100644
--- a/test/regress/regress0/bv/bool-to-bv.smt2
+++ b/test/regress/regress0/bv/bool-to-bv.smt2
@@ -6,7 +6,14 @@
 (declare-fun x0 () (_ BitVec 3))
 (declare-fun b1 () Bool)
 (declare-fun b2 () Bool)
+(declare-fun b3 () Bool)
 (assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
+(assert (not (bvslt (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
 (assert (= #b000 x2))
 (assert (=> b1 b2))
+(assert (and b1 b2))
+(assert (or b1 b2))
+(assert (xor b1 b3))
+(assert (not (xor b2 b2)))
+(assert (ite b2 b2 b1))
 (check-sat)
diff --git a/test/regress/regress0/bv/bv-to-bool.smt b/test/regress/regress0/bv/bv-to-bool1.smt
index ef4cec257..ef4cec257 100644
--- a/test/regress/regress0/bv/bv-to-bool.smt
+++ b/test/regress/regress0/bv/bv-to-bool1.smt
diff --git a/test/regress/regress0/bv/bv-to-bool2.smt2 b/test/regress/regress0/bv/bv-to-bool2.smt2
new file mode 100644
index 000000000..fb741733d
--- /dev/null
+++ b/test/regress/regress0/bv/bv-to-bool2.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --bv-to-bool
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun v1 () (_ BitVec 1))
+(declare-fun v2 () (_ BitVec 1))
+
+(assert (= (bvxor v2 v1) v1))
+
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/quantifiers/macros-real-arg.smt2 b/test/regress/regress0/quantifiers/macros-real-arg.smt2
index edacdbe37..52eeedae6 100644
--- a/test/regress/regress0/quantifiers/macros-real-arg.smt2
+++ b/test/regress/regress0/quantifiers/macros-real-arg.smt2
@@ -3,7 +3,8 @@
 ; this will fail if type rule for APPLY_UF is made strict
 (set-logic UFLIRA)
 (declare-fun P (Int) Bool)
-(assert (forall ((x Int)) (P x)))
+(declare-fun Q (Int) Bool)
+(assert (and (forall ((x Int)) (P x)) (forall ((x Int)) (Q x))))
 (declare-fun k () Real)
 (declare-fun k2 () Int)
 (assert (or (not (P (to_int k))) (not (P k2))))