From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 17 May 2013 12:59:25 +0000 (-0400)
Subject: Disallow construction of (_ BitVec 0).
X-Git-Tag: cvc5-1.0.0~7287^2~113^2~10
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=067f3f556a84c1af54d4ef2188d1b145d02b26e3;p=cvc5.git

Disallow construction of (_ BitVec 0).

Thanks to David Cok for reporting this issue.
---

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 217e7ab97..778b85fce 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1184,7 +1184,11 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
 
     /* bitvector types */
   | BITVECTOR_TOK LPAREN k=numeral RPAREN
-    { t = EXPR_MANAGER->mkBitVectorType(k); }
+    { if(k == 0) {
+        PARSER_STATE->parseError("Illegal bitvector size: 0");
+      }
+      t = EXPR_MANAGER->mkBitVectorType(k);
+    }
 
     /* basic types */
   | BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); }
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 76708807f..6c98a5529 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1204,6 +1204,9 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
         if( numerals.size() != 1 ) {
           PARSER_STATE->parseError("Illegal bitvector type.");
         }
+        if(numerals.front() == 0) {
+          PARSER_STATE->parseError("Illegal bitvector size: 0");
+        }
         t = EXPR_MANAGER->mkBitVectorType(numerals.front());
       } else {
         std::stringstream ss;