BV: Add missing type check for INT_TO_BITVECTOR. (#4613)

Fixes #4130.
This further makes an attempt at more consistent error printing.

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 96ba1bc93dd6714edcda7412fd9be5915e6a9bcd..3310a75bfb05953b9d3f708ca562bc1ce8d80a50 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -57,9 +57,9 @@ int main(int argc, char* argv[]) {
 #ifdef CVC4_COMPETITION_MODE
     *opts.getOut() << "unknown" << endl;
 #endif
-    cerr << "CVC4 Error:" << endl << e << endl << endl
-         << "Please use --help to get help on command-line options."
-         << endl;
+    cerr << "(error \"" << e << "\")" << endl
+         << endl
+         << "Please use --help to get help on command-line options." << endl;
   } catch(Exception& e) {
 #ifdef CVC4_COMPETITION_MODE
     *opts.getOut() << "unknown" << endl;
@@ -68,7 +68,7 @@ int main(int argc, char* argv[]) {
     {
       *opts.getOut() << "(error \"" << e << "\")" << endl;
     } else {
-      *opts.getErr() << "CVC4 Error:" << endl << e << endl;
+      *opts.getErr() << "(error \"" << e << "\")" << endl;
     }
     if(opts.getStatistics() && pExecutor != NULL) {
       pTotalTime->stop();

diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 97b7a8a8f0b092647c6a25a68ec119a2e76569a1..42b90cd29522ccad4c94c27bda02d1fa224ac561 100644 (file)
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -339,6 +339,10 @@ class IntToBitVectorOpTypeRule
     if (n.getKind() == kind::INT_TO_BITVECTOR_OP)
     {
       size_t bvSize = n.getConst<IntToBitVector>();
+      if (bvSize == 0)
+      {
+        throw TypeCheckingExceptionPrivate(n, "expecting bit-width > 0");
+      }
       return nodeManager->mkFunctionType(nodeManager->integerType(),
                                          nodeManager->mkBitVectorType(bvSize));
     }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fb0b381431ab1097b145a13145217d4599358d88..0e6fc26461db720bdb11434f77746e3d44d88d0f 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -360,6 +360,7 @@ set(regress_0_tests
   regress0/bv/fuzz40.smtv1.smt2
   regress0/bv/fuzz41.smtv1.smt2
   regress0/bv/issue3621.smt2
+  regress0/bv/issue-4130.smt2
   regress0/bv/int_to_bv_err_on_demand_1.smt2
   regress0/bv/mul-neg-unsat.smt2
   regress0/bv/mul-negpow2.smt2

diff --git a/test/regress/regress0/bv/issue-4130.smt2 b/test/regress/regress0/bv/issue-4130.smt2
new file mode 100644 (file)
index 0000000..aa4a130
--- /dev/null
+++ b/test/regress/regress0/bv/issue-4130.smt2
@@ -0,0 +1,10 @@
+; EXPECT: (error "Parse Error: issue-4130.smt2:9.39: expecting bit-width > 0
+; EXPECT:
+; EXPECT:   (assert (and (= a (bv2nat ((_ int2bv 0) a)))))
+; EXPECT:                                        ^
+; EXPECT: ")
+; EXIT: 1
+(set-logic ALL)
+(declare-fun a () Int)
+(assert (and (= a (bv2nat ((_ int2bv 0) a)))))
+(check-sat)

diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
index 1b5690d3a4307b3d44c352bd15dcd6c1665c7d58..848ae03492788c0aa5a995f2cd322dfa5eecc58e 100644 (file)
--- a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
+++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
@@ -1,10 +1,10 @@
 ; REQUIRES: no-competition
 ; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2
-; EXPECT-ERROR: CVC4 Error:
-; EXPECT-ERROR: Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type
+; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type
 ; EXPECT-ERROR: 
 ; EXPECT-ERROR: (Op2 <O2> <F>)
 ; EXPECT-ERROR: ^
+; EXPECT-ERROR: ")
 ; EXIT: 1
 (set-logic ALL)
 (set-option :lang sygus2)