Fix regression (#3827)

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 03f55c0595e46fa9f4a604daa891947ee5cb3856..033a50916a76496560f74d1b126a16e8676ee5f4 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -622,7 +622,7 @@ int TheoryBV::getReduction(int effort, Node n, Node& nr)
   }
   else if (n.getKind() == kind::INT_TO_BITVECTOR)
   {
-    nr = utils::eliminateBv2Nat(n);
+    nr = utils::eliminateInt2Bv(n);
     return -1;
   }
   return 0;

diff --git a/test/regress/regress1/bv/issue3654.smt2 b/test/regress/regress1/bv/issue3654.smt2
index 59c11456f9e34a241cf2cc2bf7964f5115baec05..a1e2f8b875f54ef8934febd63903647a91e4df57 100644 (file)
--- a/test/regress/regress1/bv/issue3654.smt2
+++ b/test/regress/regress1/bv/issue3654.smt2
@@ -1,4 +1,4 @@
-; COMMAND_LINE: --ext-rew-prep
+; COMMAND-LINE: --ext-rew-prep
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 4))

diff --git a/test/regress/regress1/bv/issue3776.smt2 b/test/regress/regress1/bv/issue3776.smt2
index 215f3e253b917a36fea97a906e930658ababf474..30c034c7044670c4dc1b614f2652a4b99b990a0c 100644 (file)
--- a/test/regress/regress1/bv/issue3776.smt2
+++ b/test/regress/regress1/bv/issue3776.smt2
@@ -1,4 +1,4 @@
-; COMMAND_LINE: --rewrite-divk
+; COMMAND-LINE: --rewrite-divk
 ; EXPECT: sat
 (set-logic QF_BVLIA)
 (declare-fun t () Int)

diff --git a/test/regress/regress1/sygus/issue3802-default-consts.sy b/test/regress/regress1/sygus/issue3802-default-consts.sy
index 10daee6ece89ac7bb47217d2a77c8597afcb8702..e07365052b073cdd21d428615a24cc52e4b465ae 100644 (file)
--- a/test/regress/regress1/sygus/issue3802-default-consts.sy
+++ b/test/regress/regress1/sygus/issue3802-default-consts.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
 (set-logic ALL)
 (synth-fun f 
        () Bool