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

Fixes #4130. This further makes an attempt at more consistent error printing.
CVC4 · Jun 15, 2020 · af37e2c · af37e2c
1 parent 5de97c3
commit af37e2c
Show file tree

Hide file tree

Showing 5 changed files with 21 additions and 6 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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)