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 42401268d9966d248d1e7fd478bf4380426a2cd9..d2e3a61fd6f9d6613e4da2af430cf95f1b90a5c5 100644 (file)
--- 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 55fe30b14aa95c383b917279f9d407865aac1f0c..9c596621174ae14ef66a0907b897f1a7d3acab80 100644 (file)
--- 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 (file)
index 0000000..848567e
--- /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 (file)
index 0000000..ebf103c
--- /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)