From 8f3605938d55e4278e3b386fb5d13ea09e9bf43e Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 20 Sep 2009 15:47:09 +0000
Subject: [PATCH] * Don't allow creation of zero-width bitvector literals.
 Previously bv0[0] would parse via the SMTLIB input language * If
 optimisations were disabled, sign_extend[0], would segfault in the
 bitblaster.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@243 e59a4935-1847-0410-ae03-e826735625c1
---
 src/AST/AST.cpp         | 4 ++++
 src/to-sat/BitBlast.cpp | 3 +++
 2 files changed, 7 insertions(+)

diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp
index ee5a4a2..e7f5aed 100644
--- a/src/AST/AST.cpp
+++ b/src/AST/AST.cpp
@@ -365,6 +365,10 @@ namespace BEEV
   ASTNode BeevMgr::CreateBVConst(string*& strval, int base, int bit_width)
   {
 
+	if (bit_width <= 0)
+	    FatalError("CreateBVConst: trying to create a bvconst of width: ", ASTUndefined, bit_width);
+
+
     if (!(2 == base || 10 == base || 16 == base))
       {
         FatalError("CreateBVConst: unsupported base: ", ASTUndefined, base);
diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index e71867a..318eaed 100644
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -20,6 +20,7 @@
 
 #include "../AST/AST.h"
 #include <cmath>
+#include <cassert>
 
 namespace BEEV
 {
@@ -169,6 +170,7 @@ namespace BEEV
           if (result_width == arg_width)
             {
               //nothing to sign extend
+			  result = arg;
               break;
             }
           else
@@ -484,6 +486,7 @@ namespace BEEV
     // lpvec(result);
     // cout << endl;
 
+    assert(!result.IsNull());
     return (BBTermMemo[term] = result);
 
   }
-- 
2.47.3