From d5023d2ec57dd741fcec1aaa5da8dedccd90aa02 Mon Sep 17 00:00:00 2001
From: yoni206 <yoni206@users.noreply.github.com>
Date: Mon, 5 Nov 2018 09:25:09 -0800
Subject: [PATCH] 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.
---
 test/regress/CMakeLists.txt                   |  5 +++-
 test/regress/regress0/bug217.smt2             |  1 +
 test/regress/regress0/bv/ackermann3.smt2      | 23 +++++++++++++++++++
 test/regress/regress0/bv/ackermann4.smt2      | 16 +++++++++++++
 test/regress/regress0/bv/bool-to-bv.smt2      |  7 ++++++
 .../bv/{bv-to-bool.smt => bv-to-bool1.smt}    |  0
 test/regress/regress0/bv/bv-to-bool2.smt2     | 11 +++++++++
 .../regress0/quantifiers/macros-real-arg.smt2 |  3 ++-
 8 files changed, 64 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress0/bv/ackermann3.smt2
 create mode 100644 test/regress/regress0/bv/ackermann4.smt2
 rename test/regress/regress0/bv/{bv-to-bool.smt => bv-to-bool1.smt} (100%)
 create mode 100644 test/regress/regress0/bv/bv-to-bool2.smt2

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
similarity index 100%
rename from test/regress/regress0/bv/bv-to-bool.smt
rename to 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))))
-- 
2.30.2