diff options
Diffstat (limited to 'src/parser/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 6 |
1 files changed, 5 insertions, 1 deletions
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(); } |