Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253)

3 files changed, 35 insertions, 0 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index a4d318067..9f547eb86 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -155,6 +155,8 @@ REG0_TESTS = \
 	regress0/bug605.cvc \
 	regress0/bug639.smt2 \
 	regress0/buggy-ite.smt2 \
+	regress0/bv/ackermann1.smt2 \
+	regress0/bv/ackermann2.smt2 \
 	regress0/bv/bool-to-bv.smt2 \
 	regress0/bv/bug260a.smt \
 	regress0/bv/bug260b.smt \
diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2
new file mode 100644
index 000000000..9b96b38c4
--- /dev/null
+++ b/test/regress/regress0/bv/ackermann1.smt2
@@ -0,0 +1,15 @@
+; 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 (f v0)) (g (f v0))))
+
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2
new file mode 100644
index 000000000..eeca505fe
--- /dev/null
+++ b/test/regress/regress0/bv/ackermann2.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores
+; EXPECT: unsat
+(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 v1 () (_ BitVec 4))
+(declare-fun f ((_ BitVec 4)) (_ BitVec 4))
+(declare-fun g ((_ BitVec 4)) (_ BitVec 4))
+(declare-fun h ((_ BitVec 4)) (_ BitVec 4))
+
+(assert (not (= (f (g (h v0))) (f (g (h v1))))))
+(assert (= v0 v1))
+
+
+(check-sat)
+(exit)