bv_to_int preprocessing pass

Introduces a preprocessing pass that translates bv problems to integer problems.

2 files changed, 26 insertions, 0 deletions

diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2
new file mode 100644
index 000000000..e3fcb1790
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_ashr.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (bvult (bvashr a b) (bvlshr a b)))
+
+(check-sat)
diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2
new file mode 100644
index 000000000..39dace123
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_shifts.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun s () (_ BitVec 64))
+(declare-fun t () (_ BitVec 64))
+(declare-fun splust () (_ BitVec 64))
+(declare-fun shift1 () (_ BitVec 64))
+(declare-fun shift2 () (_ BitVec 64))
+(declare-fun negshift1 () (_ BitVec 64))
+
+(assert (= shift1 (bvlshr s splust)))
+(assert (= shift2 (bvlshr t splust)))
+(assert (= negshift1 (bvneg shift1)))
+(assert (= splust (bvadd s t)))
+(assert (distinct negshift1 shift2))
+
+(check-sat)