From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 26 Feb 2020 21:43:07 +0000 (-0600)
Subject: Fix regression (#3827)
X-Git-Tag: cvc5-1.0.0~3593
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2405b98feeed522d7304207280591a71ee6c319a;p=cvc5.git

Fix regression (#3827)
---

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 03f55c059..033a50916 100644
--- 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 59c11456f..a1e2f8b87 100644
--- 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 215f3e253..30c034c70 100644
--- 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 10daee6ec..e07365052 100644
--- 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