From: yoni206 <yoni206@users.noreply.github.com>
Date: Tue, 17 May 2022 13:18:31 +0000 (+0300)
Subject: new test for resolved issue (#8784)
X-Git-Tag: cvc5-1.0.1~126
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2bf5c16be21169cd7edbb7862aa161e9a0a637f9;p=cvc5.git

new test for resolved issue (#8784)

#8412 is now fixed on main. This PR adds a regression from that issue.
closes #8412 .
---

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index e11f6d78b..6c88f29d1 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -277,6 +277,7 @@ set(regress_0_tests
   regress0/bv/bv_to_int_5281.smt2
   regress0/bv/bv_to_int_5293_1.smt2
   regress0/bv/bv_to_int_5293_2.smt2
+  regress0/bv/bv_to_int_8412.smt2
   regress0/bv/bv_to_int_bvmul2.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
diff --git a/test/regress/cli/regress0/bv/bv_to_int_8412.smt2 b/test/regress/cli/regress0/bv/bv_to_int_8412.smt2
new file mode 100644
index 000000000..3525c5f90
--- /dev/null
+++ b/test/regress/cli/regress0/bv/bv_to_int_8412.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --solve-bv-as-int=bitwise
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun x () (_ BitVec 2))
+(assert (distinct true (bvule (bvsdiv (_ bv0 2) x) (_ bv0 2))))
+(check-sat)
+