From 067f3f556a84c1af54d4ef2188d1b145d02b26e3 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 17 May 2013 08:59:25 -0400
Subject: [PATCH] Disallow construction of (_ BitVec 0).

Thanks to David Cok for reporting this issue.
---
 src/parser/cvc/Cvc.g   | 6 +++++-
 src/parser/smt2/Smt2.g | 3 +++
 2 files changed, 8 insertions(+), 1 deletion(-)

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;
-- 
2.30.2