From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 22 Aug 2011 15:15:00 +0000 (+0000)
Subject: Improvement.  Wrap most of the calls to bvtypecheck in assert(),  so that disabling... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ea564ffcebf666fb8ddb75d56ba5d383e90ac90e;p=francis%2Fstp.git

Improvement.  Wrap most of the calls to bvtypecheck in assert(),  so that disabling assertions will remove them. Cleanup woeful duplication.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1390 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 6a15945..62ff877 100644
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -455,10 +455,10 @@ Expr vc_readExpr(VC vc, Expr array, Expr index) {
   nodestar a = (nodestar)array;
   nodestar i = (nodestar)index;
 
-  BVTypeCheck(*a);
-  BVTypeCheck(*i);
+  assert(BVTypeCheck(*a));
+  assert(BVTypeCheck(*i));
   node o = b->CreateTerm(BEEV::READ,a->GetValueWidth(),*a,*i);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
 
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
@@ -472,12 +472,12 @@ Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue) {
   nodestar i = (nodestar)index;
   nodestar n = (nodestar)newValue;
 
-  BVTypeCheck(*a);
-  BVTypeCheck(*i);
-  BVTypeCheck(*n);
+  assert(BVTypeCheck(*a));
+  assert(BVTypeCheck(*i));
+  assert(BVTypeCheck(*n));
   node o = b->CreateTerm(BEEV::WRITE,a->GetValueWidth(),*a,*i,*n);
   o.SetIndexWidth(a->GetIndexWidth());
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
 
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
@@ -496,7 +496,7 @@ void vc_assertFormula(VC vc, Expr e, int absrefine_bucket_num) {
   if(!BEEV::is_Form_kind(a->GetKind()))
     BEEV::FatalError("Trying to assert a NON formula: ",*a);
 
-  BVTypeCheck(*a);
+  assert(BVTypeCheck(*a));
   b->AddAssert(*a, absrefine_bucket_num);
 }
 
@@ -525,7 +525,7 @@ int vc_query(VC vc, Expr e) {
     }
   //a->LispPrint(cout, 0);
   //printf("##################################################\n");
-  BVTypeCheck(*a);
+  assert(BVTypeCheck(*a));
   b->AddQuery(*a);
 
   const BEEV::ASTVec v = b->GetAsserts();
@@ -673,7 +673,7 @@ Expr vc_varExpr1(VC vc, const char* name,
 
   nodestar output = new node(o);
   ////if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  BVTypeCheck(*output);
+  assert(BVTypeCheck(*output));
 
   //store the decls in a vector for printing purposes
   decls->push_back(o);
@@ -709,7 +709,7 @@ Expr vc_varExpr(VC vc, const char * name, Type type) {
 
   nodestar output = new node(o);
   ////if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  BVTypeCheck(*output);
+  assert(BVTypeCheck(*output));
 
   //store the decls in a vector for printing purposes
   decls->push_back(o);
@@ -723,8 +723,8 @@ Expr vc_eqExpr(VC vc, Expr ccc0, Expr ccc1) {
 
   nodestar a = (nodestar)ccc0;
   nodestar aa = (nodestar)ccc1;
-  BVTypeCheck(*a);
-  BVTypeCheck(*aa);
+  assert(BVTypeCheck(*a));
+  assert(BVTypeCheck(*aa));
   node o = b->CreateNode(BEEV::EQ,*a,*aa);
 
   nodestar output = new node(o);
@@ -769,7 +769,7 @@ Expr vc_notExpr(VC vc, Expr ccc) {
   nodestar a = (nodestar)ccc;
 
   node o = b->CreateNode(BEEV::NOT,*a);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
 
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
@@ -782,7 +782,7 @@ Expr vc_andExpr(VC vc, Expr left, Expr right) {
   nodestar r = (nodestar)right;
 
   node o = b->CreateNode(BEEV::AND,*l,*r);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
 
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
@@ -795,7 +795,7 @@ Expr vc_orExpr(VC vc, Expr left, Expr right) {
   nodestar r = (nodestar)right;
 
   node o = b->CreateNode(BEEV::OR,*l,*r);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
   return output;
@@ -807,7 +807,7 @@ Expr vc_xorExpr(VC vc, Expr left, Expr right) {
   nodestar r = (nodestar)right;
 
   node o = b->CreateNode(BEEV::XOR,*l,*r);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
   return output;
@@ -823,7 +823,7 @@ Expr vc_andExprN(VC vc, Expr* cc, int n) {
     d.push_back(*c[i]);
 
   node o = b->CreateNode(BEEV::AND,d);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
 
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
@@ -840,7 +840,7 @@ Expr vc_orExprN(VC vc, Expr* cc, int n) {
     d.push_back(*c[i]);
 
   node o = b->CreateNode(BEEV::OR,d);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
 
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
@@ -856,7 +856,7 @@ Expr vc_bvPlusExprN(VC vc, int n_bits, Expr* cc, int n) {
     d.push_back(*c[i]);
 
   node o = b->CreateTerm(BEEV::BVPLUS, n_bits, d);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
 
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
@@ -870,9 +870,9 @@ Expr vc_iteExpr(VC vc, Expr cond, Expr thenpart, Expr elsepart){
   nodestar t = (nodestar)thenpart;
   nodestar e = (nodestar)elsepart;
 
-  BVTypeCheck(*c);
-  BVTypeCheck(*t);
-  BVTypeCheck(*e);
+  assert(BVTypeCheck(*c));
+  assert(BVTypeCheck(*t));
+  assert(BVTypeCheck(*e));
   node o;
   //if the user asks for a formula then produce a formula, else
   //prodcue a term
@@ -882,7 +882,7 @@ Expr vc_iteExpr(VC vc, Expr cond, Expr thenpart, Expr elsepart){
     o = b->CreateTerm(BEEV::ITE,t->GetValueWidth(),*c,*t,*e);
     o.SetIndexWidth(t->GetIndexWidth());
   }
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
   return output;
@@ -893,12 +893,12 @@ Expr vc_impliesExpr(VC vc, Expr antecedent, Expr consequent){
   nodestar c = (nodestar)antecedent;
   nodestar t = (nodestar)consequent;
 
-  BVTypeCheck(*c);
-  BVTypeCheck(*t);
+  assert(BVTypeCheck(*c));
+  assert(BVTypeCheck(*t));
   node o;
 
   o = b->CreateNode(BEEV::IMPLIES,*c,*t);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
   return output;
@@ -909,12 +909,12 @@ Expr vc_iffExpr(VC vc, Expr e0, Expr e1){
   nodestar c = (nodestar)e0;
   nodestar t = (nodestar)e1;
 
-  BVTypeCheck(*c);
-  BVTypeCheck(*t);
+  assert(BVTypeCheck(*c));
+  assert(BVTypeCheck(*t));
   node o;
 
   o = b->CreateNode(BEEV::IFF,*c,*t);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
   return output;
@@ -924,7 +924,7 @@ Expr vc_boolToBVExpr(VC vc, Expr form) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   nodestar c = (nodestar)form;
 
-  BVTypeCheck(*c);
+  assert(BVTypeCheck(*c));
   if(!is_Form_kind(c->GetKind()))
     {
       BEEV::FatalError("CInterface: vc_BoolToBVExpr: "\
@@ -936,7 +936,7 @@ Expr vc_boolToBVExpr(VC vc, Expr form) {
   node zero = b->CreateZeroConst(1);
   o = b->CreateTerm(BEEV::ITE,1,*c,one,zero);
 
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
   return output;
@@ -947,8 +947,8 @@ Expr vc_paramBoolExpr(VC vc, Expr boolvar, Expr parameter){
   nodestar c = (nodestar)boolvar;
   nodestar t = (nodestar)parameter;
 
-  BVTypeCheck(*c);
-  BVTypeCheck(*t);
+  assert(BVTypeCheck(*c));
+  assert(BVTypeCheck(*t));
   node o;
 
   o = b->CreateNode(BEEV::PARAMBOOL,*c,*t);
@@ -988,7 +988,7 @@ Expr vc_bvConstExprFromDecStr(VC vc,
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   string str(decimalInput);
   node n = b->CreateBVConst(str, 10, width);
-  BVTypeCheck(n);
+  assert(BVTypeCheck(n));
   nodestar output = new node(n);
   return output;
 }
@@ -998,7 +998,7 @@ Expr vc_bvConstExprFromStr(VC vc, const char* binary_repr) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
 
   node n = b->CreateBVConst(binary_repr,2);
-  BVTypeCheck(n);
+  assert(BVTypeCheck(n));
   nodestar output = new node(n);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
   return output;
@@ -1018,7 +1018,7 @@ Expr vc_bvConstExprFromInt(VC vc,
     BEEV::FatalError("FatalError");
   }
   node n = b->CreateBVConst(n_bits, v);
-  BVTypeCheck(n);
+  assert(BVTypeCheck(n));
   return persistNode(n);
 }
 
@@ -1028,7 +1028,7 @@ Expr vc_bvConstExprFromLL(VC vc,
   bmstar b = (bmstar)(((stpstar)vc)->bm);
 
   node n = b->CreateBVConst(n_bits, value);
-  BVTypeCheck(n);
+  assert(BVTypeCheck(n));
   nodestar output = new node(n);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
   return output;
@@ -1039,308 +1039,148 @@ Expr vc_bvConcatExpr(VC vc, Expr left, Expr right) {
   nodestar l = (nodestar)left;
   nodestar r = (nodestar)right;
 
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
+  assert(BVTypeCheck(*l));
+  assert(BVTypeCheck(*r));
   node o =
     b->CreateTerm(BEEV::BVCONCAT,
                   l->GetValueWidth()+ r->GetValueWidth(),*l,*r);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
   return output;
 }
 
-Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right){
+Expr createBinaryTerm(VC vc, int n_bits, Kind k, Expr left, Expr right){
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   nodestar l = (nodestar)left;
   nodestar r = (nodestar)right;
 
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateTerm(BEEV::BVPLUS,n_bits, *l, *r);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(*l));
+  assert(BVTypeCheck(*r));
+  node o = b->CreateTerm(k,n_bits, *l, *r);
+  assert(BVTypeCheck(o));
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
   return output;
 }
 
 
+Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right){
+    return createBinaryTerm(vc, n_bits, BEEV::BVPLUS, left, right);
+}
+
 Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right) {
   return vc_bvPlusExpr(vc, 32, left, right);
 }
 
-
 Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateTerm(BEEV::BVSUB,n_bits, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryTerm(vc, n_bits, BEEV::BVSUB, left, right);
 }
 
-
 Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right) {
   return vc_bvMinusExpr(vc, 32, left, right);
 }
 
-
 Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateTerm(BEEV::BVMULT,n_bits, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryTerm(vc, n_bits, BEEV::BVMULT, left, right);
 }
 
 Expr vc_bvDivExpr(VC vc, int n_bits, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateTerm(BEEV::BVDIV,n_bits, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryTerm(vc, n_bits, BEEV::BVDIV, left, right);
 }
 
 Expr vc_bvModExpr(VC vc, int n_bits, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateTerm(BEEV::BVMOD,n_bits, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryTerm(vc, n_bits, BEEV::BVMOD, left, right);
 }
 
 Expr vc_sbvDivExpr(VC vc, int n_bits, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateTerm(BEEV::SBVDIV,n_bits, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryTerm(vc, n_bits, BEEV::SBVDIV, left, right);
 }
 
 Expr vc_sbvModExpr(VC vc, int n_bits, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateTerm(BEEV::SBVREM,n_bits, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryTerm(vc, n_bits, BEEV::SBVREM, left, right);
 }
 
 Expr vc_bv32MultExpr(VC vc, Expr left, Expr right) {
   return vc_bvMultExpr(vc, 32, left, right);
 }
 
+Expr createBinaryNode(VC vc, Kind k, Expr left, Expr right)
+{
+    bmstar b = (bmstar)(((stpstar)vc)->bm);
+    nodestar l = (nodestar)left;
+    nodestar r = (nodestar)right;
+    assert(BVTypeCheck(*l));
+    assert(BVTypeCheck(*r));
+    node o = b->CreateNode(k, *l, *r);
+    assert(BVTypeCheck(o));
+    nodestar output = new node(o);
+    //if(cinterface_exprdelete_on)
+    //  created_exprs.push_back(output);
+    return output;
+}
 
 // unsigned comparators
 Expr vc_bvLtExpr(VC vc, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateNode(BEEV::BVLT, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryNode(vc,BEEV::BVLT,left,right);
 }
-
 Expr vc_bvLeExpr(VC vc, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateNode(BEEV::BVLE, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+  return createBinaryNode(vc,BEEV::BVLE,left,right);
 }
-
 Expr vc_bvGtExpr(VC vc, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateNode(BEEV::BVGT, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryNode(vc,BEEV::BVGT,left,right);
 }
-
 Expr vc_bvGeExpr(VC vc, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateNode(BEEV::BVGE, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryNode(vc,BEEV::BVGE,left,right);
 }
-
 // signed comparators
 Expr vc_sbvLtExpr(VC vc, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateNode(BEEV::BVSLT, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryNode(vc,BEEV::BVSLT,left,right);
 }
-
 Expr vc_sbvLeExpr(VC vc, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateNode(BEEV::BVSLE, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryNode(vc,BEEV::BVSLE,left,right);
 }
-
 Expr vc_sbvGtExpr(VC vc, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateNode(BEEV::BVSGT, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryNode(vc,BEEV::BVSGT,left,right);
 }
-
 Expr vc_sbvGeExpr(VC vc, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateNode(BEEV::BVSGE, *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryNode(vc,BEEV::BVSGE,left,right);
 }
 
 Expr vc_bvUMinusExpr(VC vc, Expr ccc) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   nodestar a = (nodestar)ccc;
-  BVTypeCheck(*a);
+  assert(BVTypeCheck(*a));
 
   node o = b->CreateTerm(BEEV::BVUMINUS, a->GetValueWidth(), *a);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
   return output;
 }
 
+// Expr createBinaryTerm(VC vc, int n_bits, Kind k, Expr left, Expr right){
+
 // bitwise operations: these are terms not formulas
 Expr vc_bvAndExpr(VC vc, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateTerm(BEEV::BVAND, (*l).GetValueWidth(), *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryTerm(vc, (*((nodestar)left)).GetValueWidth(), BEEV::BVAND,  left,  right);
 }
 
 Expr vc_bvOrExpr(VC vc, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateTerm(BEEV::BVOR, (*l).GetValueWidth(), *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryTerm(vc, (*((nodestar)left)).GetValueWidth(), BEEV::BVOR,  left,  right);
 }
 
 Expr vc_bvXorExpr(VC vc, Expr left, Expr right) {
-  bmstar b = (bmstar)(((stpstar)vc)->bm);
-  nodestar l = (nodestar)left;
-  nodestar r = (nodestar)right;
-
-  BVTypeCheck(*l);
-  BVTypeCheck(*r);
-  node o = b->CreateTerm(BEEV::BVXOR, (*l).GetValueWidth(), *l, *r);
-  BVTypeCheck(o);
-  nodestar output = new node(o);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+    return createBinaryTerm(vc, (*((nodestar)left)).GetValueWidth(), BEEV::BVXOR,  left,  right);
 }
 
 Expr vc_bvNotExpr(VC vc, Expr ccc) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   nodestar a = (nodestar)ccc;
 
-  BVTypeCheck(*a);
+  assert(BVTypeCheck(*a));
   node o = b->CreateTerm(BEEV::BVNEG, a->GetValueWidth(), *a);
-  BVTypeCheck(o);
+  assert(BVTypeCheck(o));
   nodestar output = new node(o);
   //if(cinterface_exprdelete_on) created_exprs.push_back(output);
   return output;
@@ -1349,7 +1189,7 @@ Expr vc_bvNotExpr(VC vc, Expr ccc) {
 Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr ccc) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   nodestar a = (nodestar)ccc;
-  BVTypeCheck(*a);
+  assert(BVTypeCheck(*a));
 
   //convert leftshift to bvconcat
   if(0 != sh_amt) {
@@ -1357,7 +1197,7 @@ Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr ccc) {
     node o = 
       b->CreateTerm(BEEV::BVCONCAT, 
                     a->GetValueWidth() + sh_amt, *a, len);
-    BVTypeCheck(o);
+    assert(BVTypeCheck(o));
     nodestar output = new node(o);
     //if(cinterface_exprdelete_on) created_exprs.push_back(output);
     return output;
@@ -1369,7 +1209,7 @@ Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr ccc) {
 Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr ccc) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   nodestar a = (nodestar)ccc;
-  BVTypeCheck(*a);
+  assert(BVTypeCheck(*a));
 
   unsigned int w = a->GetValueWidth();
   //the amount by which you are rightshifting