From 2bf5c16be21169cd7edbb7862aa161e9a0a637f9 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Tue, 17 May 2022 16:18:31 +0300 Subject: [PATCH] new test for resolved issue (#8784) #8412 is now fixed on main. This PR adds a regression from that issue. closes #8412 . --- test/regress/cli/CMakeLists.txt | 1 + test/regress/cli/regress0/bv/bv_to_int_8412.smt2 | 7 +++++++ 2 files changed, 8 insertions(+) create mode 100644 test/regress/cli/regress0/bv/bv_to_int_8412.smt2 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) + -- 2.30.2