Refactor bv-abstraction preprocessing pass. (#1860)

1 files changed, 24 insertions, 0 deletions

diff --git a/test/regress/regress1/bv/test-bv-abstraction.smt2 b/test/regress/regress1/bv/test-bv-abstraction.smt2
new file mode 100644
index 000000000..7a926d4be
--- /dev/null
+++ b/test/regress/regress1/bv/test-bv-abstraction.smt2
@@ -0,0 +1,24 @@
+; COMMAND-LINE: --bv-abstraction
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 8))
+(declare-fun x1 () (_ BitVec 8))
+(declare-fun y0 () (_ BitVec 8))
+(declare-fun y1 () (_ BitVec 8))
+(declare-fun y2 () (_ BitVec 8))
+(assert
+ (or
+  (= x0 (bvadd (bvmul (_ bv2 8) y0) y1))
+  (= x0 (bvadd (bvmul (_ bv2 8) y1) y2))
+  (= x0 (bvadd (bvmul (_ bv2 8) y2) y0))
+ )
+)
+(assert
+ (or
+  (= x1 (bvadd (bvadd (bvmul (_ bv3 8) y0) (bvmul (_ bv2 8) x0)) (_ bv5 8)))
+  (= x1 (bvadd (bvadd (bvmul (_ bv3 8) y1) (bvmul (_ bv2 8) x0)) (_ bv5 8)))
+  (= x1 (bvadd (bvadd (bvmul (_ bv3 8) x0) (bvmul (_ bv2 8) y2)) (_ bv5 8)))
+ )
+)
+(check-sat)
+(exit)