From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 8 Dec 2020 02:06:30 +0000 (-0800)
Subject: Disable algebraic BV subtheory by default and make experimental. (#5596)
X-Git-Tag: cvc5-1.0.0~2487
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a35585fc3b20d70f88a156cd0403f6aa5c9a0dbe;p=cvc5.git

Disable algebraic BV subtheory by default and make experimental. (#5596)

Fixes #5370, #5462.
---

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 42401268d..d2e3a61fd 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -80,11 +80,11 @@ header = "options/bv_options.h"
 
 [[option]]
   name       = "bitvectorAlgebraicSolver"
-  category   = "regular"
+  category   = "experimental"
   long       = "bv-algebraic-solver"
   type       = "bool"
-  default    = "true"
-  help       = "turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy)"
+  default    = "false"
+  help       = "turn on experimental algebraic solver for the bit-vector theory (only if --bitblast=lazy)"
 
 [[option]]
   name       = "bitvectorAlgebraicBudget"
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 55fe30b14..9c5966211 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -591,6 +591,8 @@ set(regress_0_tests
   regress0/issue5099-model-1.smt2
   regress0/issue5099-model-2.smt2
   regress0/issue5144-resetAssertions.smt2
+  regress0/issue5370.smt2
+  regress0/issue5462.smt2
   regress0/issue5540-2-dump-model.smt2
   regress0/issue5540-model-decls.smt2
   regress0/issue5550-num-children.smt2
diff --git a/test/regress/regress0/issue5370.smt2 b/test/regress/regress0/issue5370.smt2
new file mode 100644
index 000000000..848567e2c
--- /dev/null
+++ b/test/regress/regress0/issue5370.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --bv-to-bool
+; REQUIRES: symfpu
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun c () (Array (_ BitVec 2) (_ BitVec 1)))
+(declare-fun b () (Array (_ BitVec 2) (_ BitVec 1)))
+(declare-fun a () (_ BitVec 2))
+(declare-fun ag () (_ BitVec 1))
+(declare-fun ak () (_ BitVec 2))
+(assert (and (= a ((_ zero_extend 1) (select b (_ bv0 2)))) (= (_ bv1 1)
+  (bvsdiv (bvcomp a ak) (bvand (ite (= (_ bv0 1) (bvcomp ag (select c (bvadd a
+  (_ bv1 2))))) (_ bv1 1) (_ bv0 1)) (ite (= b (store (store c (bvadd a (_ bv1
+  2)) ag) ak (_ bv1 1))) (_ bv1 1) (_ bv0 1)))))))
+(check-sat)
diff --git a/test/regress/regress0/issue5462.smt2 b/test/regress/regress0/issue5462.smt2
new file mode 100644
index 000000000..ebf103c85
--- /dev/null
+++ b/test/regress/regress0/issue5462.smt2
@@ -0,0 +1,24 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Array (_ BitVec 32) (_ BitVec 4)))
+(declare-fun b () (Array (_ BitVec 32) (_ BitVec 4)))
+(declare-fun o () (_ BitVec 1))
+(declare-fun h () (_ BitVec 32))
+(declare-fun i () (_ BitVec 32))
+(declare-fun j () (_ BitVec 32))
+(declare-fun l () (_ BitVec 32))
+(declare-fun m () (_ BitVec 32))
+(assert (= (_ bv1 1) (bvmul (ite (= (_ bv1 1) (ite (= h (_ bv0 32)) (_ bv1 1)
+  (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnor (bvcomp o (ite (= l (bvor ((_
+  zero_extend 28) (select b (bvadd i (_ bv3 32)))) (bvlshr ((_ zero_extend 28)
+  (select b (bvudiv i (_ bv1 32)))) ((_ zero_extend 28) (select b (bvadd i (_
+  bv2 32))))))) (_ bv1 1) (_ bv0 1))) (bvsmod (ite (= (_ bv0 1) (ite (= i (_
+  bv1 32)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvshl (ite (= (_ bv1 1)
+  (ite (= b (store (store (store (store a (bvadd j (_ bv3 32)) (_ bv0 4))
+  (bvsdiv j (_ bv2 32)) (_ bv1 4)) (bvadd j (_ bv1 32)) (_ bv0 4)) j ((_
+  extract 3 0) l))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (ite (= (_ bv0
+  32) (bvor ((_ zero_extend 28) (select a (bvadd m (_ bv3 32)))) (bvadd (bvor
+  ((_ zero_extend 28) (select a (bvadd m (_ bv1 32)))) ((_ zero_extend 28)
+  (select a (bvnor m (_ bv0 32))))) ((_ zero_extend 28) (select a (bvadd m (_
+  bv2 32))))))) (_ bv1 1) (_ bv0 1))))))))
+(check-sat)