* Don't allow creation of zero-width bitvector literals. Previously bv0[0] would...

* 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

diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp
index ee5a4a2124253dfbedcb5463d112aa7a1a24f151..e7f5aedec2e4c43e1d363e8a74e3cfd4e2b59726 100644 (file)
--- 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 e71867a6617d68b362483ddd627110f53841d40b..318eaed8b582594395fe672babacae08a4a68326 100644 (file)
--- 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);
 
   }