bv: Rename simple solver to bitblast-internal. (#6888)

8 files changed, 8 insertions, 8 deletions

diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2
index 579e438a5..f70dc4a3d 100644
--- a/test/regress/regress0/bv/ackermann1.smt2
+++ b/test/regress/regress0/bv/ackermann1.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --bitblast=eager --no-check-models 
-; COMMAND-LINE: --bitblast=eager --bv-solver=simple --no-check-models 
+; COMMAND-LINE: --bitblast=eager --bv-solver=bitblast-internal --no-check-models 
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (set-info :smt-lib-version 2.6)
diff --git a/test/regress/regress0/bv/bool-model.smt2 b/test/regress/regress0/bv/bool-model.smt2
index f30dbef6f..2a2998b35 100644
--- a/test/regress/regress0/bv/bool-model.smt2
+++ b/test/regress/regress0/bv/bool-model.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --bitblast=eager
-; COMMAND-LINE: --bitblast=eager --bv-solver=simple
+; COMMAND-LINE: --bitblast=eager --bv-solver=bitblast-internal
 (set-info :status sat)
 (set-logic QF_BV)
 (declare-fun x () Bool)
diff --git a/test/regress/regress0/bv/bool-to-bv-ite.smt2 b/test/regress/regress0/bv/bool-to-bv-ite.smt2
index de0ec8897..09fcb4e11 100644
--- a/test/regress/regress0/bv/bool-to-bv-ite.smt2
+++ b/test/regress/regress0/bv/bool-to-bv-ite.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --bool-to-bv=ite
-; COMMAND-LINE: --bool-to-bv=ite --bv-solver=simple
+; COMMAND-LINE: --bool-to-bv=ite --bv-solver=bitblast-internal
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun x2 () (_ BitVec 3))
diff --git a/test/regress/regress0/bv/bug734.smt2 b/test/regress/regress0/bv/bug734.smt2
index 5e92036ec..0e392d3c6 100644
--- a/test/regress/regress0/bv/bug734.smt2
+++ b/test/regress/regress0/bv/bug734.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --incremental
-; COMMAND-LINE: --incremental --bv-solver=simple
+; COMMAND-LINE: --incremental --bv-solver=bitblast-internal
 ; EXPECT: sat
 ; EXPECT: sat
 (set-logic QF_BV)
diff --git a/test/regress/regress0/bv/issue-4076.smt2 b/test/regress/regress0/bv/issue-4076.smt2
index e94779439..12bc3e4ca 100644
--- a/test/regress/regress0/bv/issue-4076.smt2
+++ b/test/regress/regress0/bv/issue-4076.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --incremental
-; COMMAND-LINE: --incremental --bv-solver=simple
+; COMMAND-LINE: --incremental --bv-solver=bitblast-internal
 ; EXPECT: sat
 ; EXPECT: sat
 (set-logic ALL)
diff --git a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2
index 0c6e7e0eb..2a924dac8 100644
--- a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2
+++ b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE:
-; COMMAND-LINE: --bv-solver=simple
+; COMMAND-LINE: --bv-solver=bitblast-internal
 (set-logic QF_BV)
 (set-info :status unsat)
 (declare-const x (_ BitVec 4))
diff --git a/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2
index 98d75d74f..8cb717258 100644
--- a/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2
+++ b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bv-solver=simple
+; COMMAND-LINE: --bv-solver=bitblast-internal
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-const __ (_ BitVec 3))
diff --git a/test/regress/regress0/proofs/open-pf-rederivation.smt2 b/test/regress/regress0/proofs/open-pf-rederivation.smt2
index 7095ec942..877389184 100644
--- a/test/regress/regress0/proofs/open-pf-rederivation.smt2
+++ b/test/regress/regress0/proofs/open-pf-rederivation.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bv-solver=simple
+; COMMAND-LINE: --bv-solver=bitblast-internal
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-const __ (_ BitVec 7))