Merge branch 'master' of https://github.com/CVC4/CVC4.git

Conflicts:
	proofs/signatures/Makefile.am
	src/Makefile.am
	src/expr/datatype.cpp
	src/options/datatypes_options
	src/options/options_template.cpp
	src/options/quantifiers_options
	src/proof/arith_proof.cpp
	src/proof/arith_proof.h
	src/proof/array_proof.cpp
	src/proof/array_proof.h
	src/proof/bitvector_proof.cpp
	src/proof/bitvector_proof.h
	src/proof/cnf_proof.cpp
	src/proof/cnf_proof.h
	src/proof/proof_manager.cpp
	src/proof/proof_manager.h
	src/proof/sat_proof.h
	src/proof/sat_proof_implementation.h
	src/proof/skolemization_manager.h
	src/proof/theory_proof.cpp
	src/proof/theory_proof.h
	src/proof/uf_proof.cpp
	src/proof/uf_proof.h
	src/prop/cnf_stream.cpp
	src/prop/cnf_stream.h
	src/prop/minisat/core/Solver.cc
	src/prop/prop_engine.cpp
	src/prop/prop_engine.h
	src/prop/theory_proxy.cpp
	src/smt/smt_engine.cpp
	src/smt/smt_engine_check_proof.cpp
	src/theory/arrays/array_proof_reconstruction.cpp
	src/theory/arrays/theory_arrays.cpp
	src/theory/bv/eager_bitblaster.cpp
	src/theory/bv/lazy_bitblaster.cpp
	src/theory/datatypes/theory_datatypes.cpp
	src/theory/quantifiers/alpha_equivalence.cpp
	src/theory/quantifiers/candidate_generator.cpp
	src/theory/quantifiers/candidate_generator.h
	src/theory/quantifiers/ce_guided_single_inv.cpp
	src/theory/quantifiers/ceg_instantiator.cpp
	src/theory/quantifiers/conjecture_generator.cpp
	src/theory/quantifiers/equality_infer.cpp
	src/theory/quantifiers/equality_infer.h
	src/theory/quantifiers/inst_match_generator.cpp
	src/theory/quantifiers/inst_propagator.cpp
	src/theory/quantifiers/inst_propagator.h
	src/theory/quantifiers/inst_strategy_e_matching.cpp
	src/theory/quantifiers/inst_strategy_e_matching.h
	src/theory/quantifiers/instantiation_engine.cpp
	src/theory/quantifiers/model_builder.cpp
	src/theory/quantifiers/model_engine.cpp
	src/theory/quantifiers/quant_conflict_find.cpp
	src/theory/quantifiers/quant_conflict_find.h
	src/theory/quantifiers/quant_split.cpp
	src/theory/quantifiers/quant_util.cpp
	src/theory/quantifiers/quantifiers_rewriter.cpp
	src/theory/quantifiers/quantifiers_rewriter.h
	src/theory/quantifiers/term_database.cpp
	src/theory/quantifiers/term_database.h
	src/theory/quantifiers/trigger.cpp
	src/theory/quantifiers/trigger.h
	src/theory/quantifiers_engine.cpp
	src/theory/quantifiers_engine.h
	src/theory/sets/kinds
	src/theory/sets/theory_sets_private.cpp
	src/theory/sets/theory_sets_private.h
	src/theory/sets/theory_sets_rewriter.cpp
	src/theory/sets/theory_sets_type_rules.h
	src/theory/strings/theory_strings.cpp
	src/theory/strings/theory_strings.h
	src/theory/theory_engine.cpp
	src/theory/theory_engine.h
	src/theory/uf/equality_engine.cpp
	test/regress/regress0/fmf/Makefile.am
	test/regress/regress0/quantifiers/Makefile.am
	test/regress/regress0/strings/Makefile.am
	test/regress/regress0/sygus/Makefile.am
	test/regress/regress0/sygus/max2-univ.sy

13 files changed, 233 insertions, 739 deletions

diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp
index c96791aeb..22e326cda 100644
--- a/proofs/lfsc_checker/check.cpp
+++ b/proofs/lfsc_checker/check.cpp
@@ -24,7 +24,7 @@ int colnum = 1;
 const char *filename = 0;
 FILE *curfile = 0;
 
-//#define USE_HASH_MAPS
+//#define USE_HASH_MAPS  //AJR: deprecated
 
 symmap2 progs;
 std::vector< Expr* > ascHoles;
diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp
index ae0e49531..5cb774fbf 100644
--- a/proofs/lfsc_checker/expr.cpp
+++ b/proofs/lfsc_checker/expr.cpp
@@ -34,7 +34,6 @@ bool destroy_progs = false;
     Expr *r = rr;	    \
     int ref = r->data >> 9; \
     ref = ref - 1; \
-    r->debugrefcnt(ref,DEC); \
     if (ref == 0) {  \
       _e = r;		  \
       goto start_destroy; \
@@ -43,6 +42,7 @@ bool destroy_progs = false;
       r->data = (ref << 9) | (r->data & 511); \
   } while(0)
 
+//removed from below "ref = ref -1;":   r->debugrefcnt(ref,DEC);
 
 void Expr::destroy(Expr *_e, bool dec_kids) {
  start_destroy:
diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h
index 32a62ab33..5a505a3d9 100644
--- a/proofs/lfsc_checker/expr.h
+++ b/proofs/lfsc_checker/expr.h
@@ -8,9 +8,9 @@
 #include <map>
 #include "chunking_memory_management.h"
 
-#define USE_FLAT_APP
+#define USE_FLAT_APP  //AJR: off deprecated
 #define MARKVAR_32
-#define DEBUG_SYM_NAMES
+//#define DEBUG_SYM_NAMES
 //#define DEBUG_SYMS
 
 // Expr class
@@ -66,7 +66,6 @@ protected:
 
   enum { INC, DEC, CREATE };
   void debugrefcnt(int ref, int what) {
-#ifdef DEBUG_REFCNT
     std::cout << "[";
     debug();
     switch(what) {
@@ -83,10 +82,6 @@ protected:
     char tmp[10];
     sprintf(tmp,"%d",ref);
     std::cout << tmp << "]\n";
-#else
-    (void)ref;
-    (void)what;
-#endif
   }
 
   Expr(int _class, int _op)
@@ -114,14 +109,18 @@ public:
     //   std::cout << " " << ref << std::endl;
     //}
     ref = ref<4194303 ? ref + 1 : ref;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(ref,INC);
+#endif
     data = (ref << 9) | (data & 511);
   }
   static void destroy(Expr *, bool);
   inline void dec(bool dec_kids = true) {
     int ref = getrefcnt();
     ref = ref - 1;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(ref,DEC);
+#endif
     if (ref == 0)
       destroy(this,dec_kids);
     else
@@ -131,10 +130,10 @@ public:
   //must pass statType (the expr representing "type") to this function
   bool isType( Expr* statType );
 
-  inline bool isDatatype() {
+  inline bool isDatatype() const {
     return getclass() == SYMS_EXPR || getop() == MPZ || getop() == MPQ;
   }
-  inline bool isArithTerm() {
+  inline bool isArithTerm() const {
     return getop() == ADD || getop() == NEG;
   }
 
@@ -188,13 +187,17 @@ public:
   CExpr(int _op) : Expr(CEXPR, _op), kids() {
     kids = new Expr *[1];
     kids[0] = 0;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
   CExpr(int _op, Expr *e1) : Expr(CEXPR, _op), kids() {
     kids = new Expr *[2];
     kids[0] = e1;
     kids[1] = 0;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
   CExpr(int _op, Expr *e1, Expr *e2)
     : Expr(CEXPR, _op), kids() {
@@ -202,7 +205,9 @@ public:
     kids[0] = e1;
     kids[1] = e2;
     kids[2] = 0;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
   CExpr(int _op, Expr *e1, Expr *e2, Expr *e3)
     : Expr(CEXPR, _op), kids() {
@@ -211,7 +216,9 @@ public:
     kids[1] = e2;
     kids[2] = e3;
     kids[3] = 0;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
   CExpr(int _op, Expr *e1, Expr *e2, Expr *e3, Expr *e4)
     : Expr(CEXPR, _op), kids() {
@@ -221,7 +228,9 @@ public:
     kids[2] = e3;
     kids[3] = e4;
     kids[4] = 0;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
   CExpr(int _op, const std::vector<Expr *> &_kids) 
     : Expr(CEXPR, _op), kids() {
@@ -230,13 +239,17 @@ public:
     for (i = 0; i < iend; i++)
       kids[i] = _kids[i];
     kids[i] = 0;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
 
   // _kids must be null-terminated.
   CExpr(int _op, bool dummy, Expr **_kids) : Expr(CEXPR, _op), kids(_kids) {
     (void)dummy;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
 
   Expr *whr();
@@ -253,7 +266,9 @@ class IntExpr : public Expr {
   }
   IntExpr(mpz_t _n) : Expr(INT_EXPR, 0), n() {
     mpz_init_set(n,_n);
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
   IntExpr(signed long int _n ) : Expr(INT_EXPR, 0), n() {
     mpz_init_set_si( n, _n );
@@ -271,7 +286,9 @@ class RatExpr : public Expr {
   RatExpr(mpq_t _n) : Expr(RAT_EXPR, 0), n() {
     mpq_init( n );
     mpq_set(n,_n);
+#ifdef DEBUG_REFCNT   
     debugrefcnt(1,CREATE);
+#endif
     mpq_canonicalize( n );
   }
   RatExpr(signed long int _n1, unsigned long int _n2 ) : Expr(RAT_EXPR, 0), n() {
@@ -290,15 +307,19 @@ class SymExpr : public Expr {
     : Expr(theclass, 0), val(0)
   {   
     (void)_s;
+#ifdef DEBUG_REFCNT   
     if (theclass == SYM_EXPR)
       debugrefcnt(1,CREATE);
+#endif
   }
   SymExpr(const SymExpr &e, int theclass = SYM_EXPR) 
     : Expr(theclass, 0), val(0)
   {
     (void)e;
+#ifdef DEBUG_REFCNT   
     if (theclass == SYM_EXPR)
       debugrefcnt(1,CREATE);
+#endif
   }
 #ifdef MARKVAR_32
 private:
@@ -317,12 +338,16 @@ class SymSExpr : public SymExpr {
   SymSExpr(std::string _s, int theclass = SYMS_EXPR) 
     : SymExpr(_s, theclass), s(_s)
   {
+#ifdef DEBUG_REFCNT   
     debugrefcnt(1,CREATE);
+#endif
   }
   SymSExpr(const SymSExpr &e, int theclass = SYMS_EXPR) 
     : SymExpr(e, theclass), s(e.s)
   { 
+#ifdef DEBUG_REFCNT   
     debugrefcnt(1,CREATE);
+#endif
   }
 };
 
@@ -338,7 +363,9 @@ public:
 #ifdef DEBUG_HOLE_NAMES
     id = next_id++;
 #endif
+#ifdef DEBUG_REFCNT   
     debugrefcnt(1,CREATE);
+#endif
   }
   Expr *val; // may be set during subst(), defeq(), and clone().
 };
diff --git a/proofs/lfsc_checker/main.cpp b/proofs/lfsc_checker/main.cpp
index 80f36e69f..1d8ba5809 100644
--- a/proofs/lfsc_checker/main.cpp
+++ b/proofs/lfsc_checker/main.cpp
@@ -133,6 +133,7 @@ int main(int argc, char **argv) {
   a.files.clear();
 #endif
 
+  std::cout << "Proof checked successfully!" << std::endl << std::endl;
   std::cout << "time = " << (int)clock() - check_time << std::endl;
   std::cout << "sym count = " << SymExpr::symmCount << std::endl;
   std::cout << "marked count = " << Expr::markedCount << std::endl;
diff --git a/proofs/lfsc_checker/scccode.cpp b/proofs/lfsc_checker/scccode.cpp
index 22f26ec88..19712579c 100644
--- a/proofs/lfsc_checker/scccode.cpp
+++ b/proofs/lfsc_checker/scccode.cpp
@@ -1,609 +1,11 @@
 #include "scccode.h"
 
-Expr* e_pos;
-Expr* e_neg;
-Expr* e_tt;
-Expr* e_ff;
-Expr* e_cln;
-Expr* e_clc;
-Expr* e_concat;
-Expr* e_clr;
-Expr* e_litvar;
-Expr* e_litpol;
-Expr* e_notb;
-Expr* e_iffb;
-Expr* e_clear_mark;
-Expr* e_append;
-Expr* e_simplify_clause_h;
-Expr* e_simplify_clause;
-
 void init_compiled_scc(){
-   e_pos = symbols->get("pos").first;
-   e_neg = symbols->get("neg").first;
-   e_tt = symbols->get("tt").first;
-   e_ff = symbols->get("ff").first;
-   e_cln = symbols->get("cln").first;
-   e_clc = symbols->get("clc").first;
-   e_concat = symbols->get("concat").first;
-   e_clr = symbols->get("clr").first;
-   e_litvar = progs["litvar"];
-   e_litpol = progs["litpol"];
-   e_notb = progs["notb"];
-   e_iffb = progs["iffb"];
-   e_clear_mark = progs["clear_mark"];
-   e_append = progs["append"];
-   e_simplify_clause_h = progs["simplify_clause_h"];
-   e_simplify_clause = progs["simplify_clause"];
-}
-
-Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){
-   if( p==e_litvar ){
-      return f_litvar( args[0] );
-   }else if( p==e_litpol ){
-      return f_litpol( args[0] );
-   }else if( p==e_notb ){
-      return f_notb( args[0] );
-   }else if( p==e_iffb ){
-      return f_iffb( args[0], args[1] );
-   }else if( p==e_clear_mark ){
-      return f_clear_mark( args[0] );
-   }else if( p==e_append ){
-      return f_append( args[0], args[1] );
-   }else if( p==e_simplify_clause_h ){
-      return f_simplify_clause_h( args[0], args[1] );
-   }else if( p==e_simplify_clause ){
-      return f_simplify_clause( args[0] );
-   }else{
-      return NULL;
-   }
-}
-
-Expr* f_litvar( Expr* l ){
-   Expr* e0;
-   l->inc();
-   Expr* e1 = l->followDefs()->get_head();
-   Expr* e2;
-   e2 = e_pos;
-   e2->inc();
-   Expr* e3;
-   e3 = e_neg;
-   e3->inc();
-   if( e1==e2 ){
-      Expr* x = ((CExpr*)l->followDefs())->kids[1];
-      e0 = x;
-      e0->inc();
-   }else if( e1==e3 ){
-      Expr* x = ((CExpr*)l->followDefs())->kids[1];
-      e0 = x;
-      e0->inc();
-   }else{
-      std::cout << "Could not find match for expression in function f_litvar ";
-      e1->print( std::cout );
-      std::cout << std::endl;
-      exit( 1 );
-   }
-   l->dec();
-   e2->dec();
-   e3->dec();
-   return e0;
-}
-
-Expr* f_litpol( Expr* l ){
-   Expr* e0;
-   l->inc();
-   Expr* e1 = l->followDefs()->get_head();
-   Expr* e2;
-   e2 = e_pos;
-   e2->inc();
-   Expr* e3;
-   e3 = e_neg;
-   e3->inc();
-   if( e1==e2 ){
-      // Expr* x = ((CExpr*)l->followDefs())->kids[1];
-      e0 = e_tt;
-      e0->inc();
-   }else if( e1==e3 ){
-      // Expr* x = ((CExpr*)l->followDefs())->kids[1];
-      e0 = e_ff;
-      e0->inc();
-   }else{
-      std::cout << "Could not find match for expression in function f_litpol ";
-      e1->print( std::cout );
-      std::cout << std::endl;
-      exit( 1 );
-   }
-   l->dec();
-   e2->dec();
-   e3->dec();
-   return e0;
-}
 
-Expr* f_notb( Expr* b ){
-   Expr* e0;
-   b->inc();
-   Expr* e1 = b->followDefs()->get_head();
-   Expr* e2;
-   e2 = e_ff;
-   e2->inc();
-   Expr* e3;
-   e3 = e_tt;
-   e3->inc();
-   if( e1==e2 ){
-      e0 = e_tt;
-      e0->inc();
-   }else if( e1==e3 ){
-      e0 = e_ff;
-      e0->inc();
-   }else{
-      std::cout << "Could not find match for expression in function f_notb ";
-      e1->print( std::cout );
-      std::cout << std::endl;
-      exit( 1 );
-   }
-   b->dec();
-   e2->dec();
-   e3->dec();
-   return e0;
 }
 
-Expr* f_iffb( Expr* b1, Expr* b2 ){
-   Expr* e0;
-   b1->inc();
-   Expr* e1 = b1->followDefs()->get_head();
-   Expr* e2;
-   e2 = e_tt;
-   e2->inc();
-   Expr* e3;
-   e3 = e_ff;
-   e3->inc();
-   if( e1==e2 ){
-      e0 = b2;
-      e0->inc();
-   }else if( e1==e3 ){
-      b2->inc();
-      e0 = f_notb( b2 );
-      b2->dec();
-   }else{
-      std::cout << "Could not find match for expression in function f_iffb ";
-      e1->print( std::cout );
-      std::cout << std::endl;
-      exit( 1 );
-   }
-   b1->dec();
-   e2->dec();
-   e3->dec();
-   return e0;
-}
-
-Expr* f_clear_mark( Expr* v ){
-   Expr* e0;
-   v->inc();
-   if ( ((SymExpr*)v->followDefs())->getmark(0)){
-      v->inc();
-      if ( ((SymExpr*)v->followDefs())->getmark(0))
-         ((SymExpr*)v->followDefs())->clearmark(0);
-      else
-         ((SymExpr*)v->followDefs())->setmark(0);
-      e0 = v;
-      e0->inc();
-      v->dec();
-   }else{
-      e0 = v;
-      e0->inc();
-   }
-   v->dec();
-   return e0;
-}
-
-Expr* f_append( Expr* c1, Expr* c2 ){
-   Expr* e0;
-   c1->inc();
-   Expr* e1 = c1->followDefs()->get_head();
-   Expr* e2;
-   e2 = e_cln;
-   e2->inc();
-   Expr* e3;
-   e3 = e_clc;
-   e3->inc();
-   if( e1==e2 ){
-      e0 = c2;
-      e0->inc();
-   }else if( e1==e3 ){
-      Expr* l = ((CExpr*)c1->followDefs())->kids[1];
-      Expr* c1h = ((CExpr*)c1->followDefs())->kids[2];
-      l->inc();
-      Expr* e4;
-      c1h->inc();
-      c2->inc();
-      e4 = f_append( c1h, c2 );
-      c1h->dec();
-      c2->dec();
-      static Expr* e5;
-      e5 = e_clc;
-      e5->inc();
-      e0 = new CExpr( APP, e5, l, e4 );
-   }else{
-      std::cout << "Could not find match for expression in function f_append ";
-      e1->print( std::cout );
-      std::cout << std::endl;
-      exit( 1 );
-   }
-   c1->dec();
-   e2->dec();
-   e3->dec();
-   return e0;
-}
-
-Expr* f_simplify_clause_h( Expr* pol, Expr* c ){
-   Expr* e0;
-   c->inc();
-   Expr* e1 = c->followDefs()->get_head();
-   Expr* e2;
-   e2 = e_cln;
-   e2->inc();
-   Expr* e3;
-   e3 = e_clc;
-   e3->inc();
-   Expr* e4;
-   e4 = e_concat;
-   e4->inc();
-   Expr* e5;
-   e5 = e_clr;
-   e5->inc();
-   if( e1==e2 ){
-      e0 = e_cln;
-      e0->inc();
-   }else if( e1==e3 ){
-      Expr* l = ((CExpr*)c->followDefs())->kids[1];
-      Expr* c1 = ((CExpr*)c->followDefs())->kids[2];
-      Expr* v;
-      l->inc();
-      v = f_litvar( l );
-      l->dec();
-      Expr* e6;
-      Expr* e7;
-      l->inc();
-      e7 = f_litpol( l );
-      l->dec();
-      pol->inc();
-      e6 = f_iffb( e7, pol );
-      e7->dec();
-      pol->dec();
-      Expr* e8 = e6->followDefs()->get_head();
-      Expr* e9;
-      e9 = e_tt;
-      e9->inc();
-      Expr* e10;
-      e10 = e_ff;
-      e10->inc();
-      if( e8==e9 ){
-         Expr* m;
-         v->inc();
-         if ( ((SymExpr*)v->followDefs())->getmark(0)){
-            m = e_tt;
-            m->inc();
-         }else{
-            Expr* e11;
-            v->inc();
-            if ( ((SymExpr*)v->followDefs())->getmark(0))
-               ((SymExpr*)v->followDefs())->clearmark(0);
-            else
-               ((SymExpr*)v->followDefs())->setmark(0);
-            e11 = v;
-            e11->inc();
-            v->dec();
-            e11->dec();
-            m = e_ff;
-            m->inc();
-         }
-         v->dec();
-         Expr* ch;
-         pol->inc();
-         c1->inc();
-         ch = f_simplify_clause_h( pol, c1 );
-         pol->dec();
-         c1->dec();
-         m->inc();
-         Expr* e12 = m->followDefs()->get_head();
-         Expr* e13;
-         e13 = e_tt;
-         e13->inc();
-         Expr* e14;
-         e14 = e_ff;
-         e14->inc();
-         if( e12==e13 ){
-            Expr* e15;
-            v->inc();
-            if ( ((SymExpr*)v->followDefs())->getmark(1)){
-               e15 = v;
-               e15->inc();
-            }else{
-               v->inc();
-               if ( ((SymExpr*)v->followDefs())->getmark(1))
-                  ((SymExpr*)v->followDefs())->clearmark(1);
-               else
-                  ((SymExpr*)v->followDefs())->setmark(1);
-               e15 = v;
-               e15->inc();
-               v->dec();
-            }
-            v->dec();
-            e15->dec();
-            e0 = ch;
-            e0->inc();
-         }else if( e12==e14 ){
-            Expr* e16;
-            Expr* e17;
-            v->inc();
-            if ( ((SymExpr*)v->followDefs())->getmark(1)){
-               v->inc();
-               if ( ((SymExpr*)v->followDefs())->getmark(1))
-                  ((SymExpr*)v->followDefs())->clearmark(1);
-               else
-                  ((SymExpr*)v->followDefs())->setmark(1);
-               e17 = v;
-               e17->inc();
-               v->dec();
-            }else{
-               e17 = v;
-               e17->inc();
-            }
-            v->dec();
-            e17->dec();
-            v->inc();
-            if ( ((SymExpr*)v->followDefs())->getmark(0))
-               ((SymExpr*)v->followDefs())->clearmark(0);
-            else
-               ((SymExpr*)v->followDefs())->setmark(0);
-            e16 = v;
-            e16->inc();
-            v->dec();
-            e16->dec();
-            l->inc();
-            ch->inc();
-            static Expr* e18;
-            e18 = e_clc;
-            e18->inc();
-            e0 = new CExpr( APP, e18, l, ch );
-         }else{
-            std::cout << "Could not find match for expression in function f_simplify_clause_h ";
-            e12->print( std::cout );
-            std::cout << std::endl;
-            exit( 1 );
-         }
-         m->dec();
-         e13->dec();
-         e14->dec();
-         ch->dec();
-         m->dec();
-      }else if( e8==e10 ){
-         l->inc();
-         Expr* e19;
-         pol->inc();
-         c1->inc();
-         e19 = f_simplify_clause_h( pol, c1 );
-         pol->dec();
-         c1->dec();
-         static Expr* e20;
-         e20 = e_clc;
-         e20->inc();
-         e0 = new CExpr( APP, e20, l, e19 );
-      }else{
-         std::cout << "Could not find match for expression in function f_simplify_clause_h ";
-         e8->print( std::cout );
-         std::cout << std::endl;
-         exit( 1 );
-      }
-      e6->dec();
-      e9->dec();
-      e10->dec();
-      v->dec();
-   }else if( e1==e4 ){
-      Expr* c1 = ((CExpr*)c->followDefs())->kids[1];
-      Expr* c2 = ((CExpr*)c->followDefs())->kids[2];
-      pol->inc();
-      Expr* e21 = pol->followDefs()->get_head();
-      Expr* e22;
-      e22 = e_ff;
-      e22->inc();
-      Expr* e23;
-      e23 = e_tt;
-      e23->inc();
-      if( e21==e22 ){
-         Expr* e24;
-         pol->inc();
-         c1->inc();
-         e24 = f_simplify_clause_h( pol, c1 );
-         pol->dec();
-         c1->dec();
-         Expr* e25;
-         pol->inc();
-         c2->inc();
-         e25 = f_simplify_clause_h( pol, c2 );
-         pol->dec();
-         c2->dec();
-         static Expr* e26;
-         e26 = e_concat;
-         e26->inc();
-         e0 = new CExpr( APP, e26, e24, e25 );
-      }else if( e21==e23 ){
-         Expr* e27;
-         pol->inc();
-         c1->inc();
-         e27 = f_simplify_clause_h( pol, c1 );
-         pol->dec();
-         c1->dec();
-         Expr* e28;
-         pol->inc();
-         c2->inc();
-         e28 = f_simplify_clause_h( pol, c2 );
-         pol->dec();
-         c2->dec();
-         e0 = f_append( e27, e28 );
-         e27->dec();
-         e28->dec();
-      }else{
-         std::cout << "Could not find match for expression in function f_simplify_clause_h ";
-         e21->print( std::cout );
-         std::cout << std::endl;
-         exit( 1 );
-      }
-      pol->dec();
-      e22->dec();
-      e23->dec();
-   }else if( e1==e5 ){
-      Expr* l = ((CExpr*)c->followDefs())->kids[1];
-      Expr* c1 = ((CExpr*)c->followDefs())->kids[2];
-      Expr* e29;
-      Expr* e30;
-      l->inc();
-      e30 = f_litpol( l );
-      l->dec();
-      pol->inc();
-      e29 = f_iffb( e30, pol );
-      e30->dec();
-      pol->dec();
-      Expr* e31 = e29->followDefs()->get_head();
-      Expr* e32;
-      e32 = e_ff;
-      e32->inc();
-      Expr* e33;
-      e33 = e_tt;
-      e33->inc();
-      if( e31==e32 ){
-         l->inc();
-         Expr* e34;
-         pol->inc();
-         c1->inc();
-         e34 = f_simplify_clause_h( pol, c1 );
-         pol->dec();
-         c1->dec();
-         static Expr* e35;
-         e35 = e_clr;
-         e35->inc();
-         e0 = new CExpr( APP, e35, l, e34 );
-      }else if( e31==e33 ){
-         Expr* v;
-         l->inc();
-         v = f_litvar( l );
-         l->dec();
-         Expr* m;
-         v->inc();
-         if ( ((SymExpr*)v->followDefs())->getmark(0)){
-            m = e_tt;
-            m->inc();
-         }else{
-            Expr* e36;
-            v->inc();
-            if ( ((SymExpr*)v->followDefs())->getmark(0))
-               ((SymExpr*)v->followDefs())->clearmark(0);
-            else
-               ((SymExpr*)v->followDefs())->setmark(0);
-            e36 = v;
-            e36->inc();
-            v->dec();
-            e36->dec();
-            m = e_ff;
-            m->inc();
-         }
-         v->dec();
-         Expr* ch;
-         pol->inc();
-         c1->inc();
-         ch = f_simplify_clause_h( pol, c1 );
-         pol->dec();
-         c1->dec();
-         v->inc();
-         if ( ((SymExpr*)v->followDefs())->getmark(1)){
-            m->inc();
-            Expr* e37 = m->followDefs()->get_head();
-            Expr* e38;
-            e38 = e_tt;
-            e38->inc();
-            Expr* e39;
-            e39 = e_ff;
-            e39->inc();
-            if( e37==e38 ){
-               e0 = ch;
-               e0->inc();
-            }else if( e37==e39 ){
-               Expr* e40;
-               Expr* e41;
-               v->inc();
-               if ( ((SymExpr*)v->followDefs())->getmark(1))
-                  ((SymExpr*)v->followDefs())->clearmark(1);
-               else
-                  ((SymExpr*)v->followDefs())->setmark(1);
-               e41 = v;
-               e41->inc();
-               v->dec();
-               e41->dec();
-               v->inc();
-               if ( ((SymExpr*)v->followDefs())->getmark(0))
-                  ((SymExpr*)v->followDefs())->clearmark(0);
-               else
-                  ((SymExpr*)v->followDefs())->setmark(0);
-               e40 = v;
-               e40->inc();
-               v->dec();
-               e40->dec();
-               e0 = ch;
-               e0->inc();
-            }else{
-               std::cout << "Could not find match for expression in function f_simplify_clause_h ";
-               e37->print( std::cout );
-               std::cout << std::endl;
-               exit( 1 );
-            }
-            m->dec();
-            e38->dec();
-            e39->dec();
-         }else{
-            e0 = NULL;
-         }
-         v->dec();
-         ch->dec();
-         m->dec();
-         v->dec();
-      }else{
-         std::cout << "Could not find match for expression in function f_simplify_clause_h ";
-         e31->print( std::cout );
-         std::cout << std::endl;
-         exit( 1 );
-      }
-      e29->dec();
-      e32->dec();
-      e33->dec();
-   }else{
-      std::cout << "Could not find match for expression in function f_simplify_clause_h ";
-      e1->print( std::cout );
-      std::cout << std::endl;
-      exit( 1 );
-   }
-   c->dec();
-   e2->dec();
-   e3->dec();
-   e4->dec();
-   e5->dec();
-   return e0;
+Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){
+  return NULL;
 }
 
-Expr* f_simplify_clause( Expr* c ){
-   Expr* e0;
-   static Expr* e1;
-   e1 = e_tt;
-   e1->inc();
-   Expr* e2;
-   static Expr* e3;
-   e3 = e_ff;
-   e3->inc();
-   c->inc();
-   e2 = f_simplify_clause_h( e3, c );
-   e3->dec();
-   c->dec();
-   e0 = f_simplify_clause_h( e1, e2 );
-   e1->dec();
-   e2->dec();
-   return e0;
-}
 
diff --git a/proofs/lfsc_checker/scccode.h b/proofs/lfsc_checker/scccode.h
index 6f5efc8b5..2ab549c10 100644
--- a/proofs/lfsc_checker/scccode.h
+++ b/proofs/lfsc_checker/scccode.h
@@ -7,21 +7,5 @@ void init_compiled_scc();
 
 Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args );
 
-inline Expr* f_litvar( Expr* l );
-
-inline Expr* f_litpol( Expr* l );
-
-inline Expr* f_notb( Expr* b );
-
-inline Expr* f_iffb( Expr* b1, Expr* b2 );
-
-inline Expr* f_clear_mark( Expr* v );
-
-inline Expr* f_append( Expr* c1, Expr* c2 );
-
-inline Expr* f_simplify_clause_h( Expr* pol, Expr* c );
-
-inline Expr* f_simplify_clause( Expr* c );
-
 #endif
 
diff --git a/proofs/lfsc_checker/sccwriter.cpp b/proofs/lfsc_checker/sccwriter.cpp
index 5c1da2a3f..d93341ab8 100644
--- a/proofs/lfsc_checker/sccwriter.cpp
+++ b/proofs/lfsc_checker/sccwriter.cpp
@@ -286,7 +286,7 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r
     {
       indent( os, ind );
       os << retModString.c_str();
-      os << "new IntExpr( " << mpz_get_si( ((IntExpr*)code)->n ) << " );" << std::endl;
+      os << "new IntExpr( (signed long int)" << mpz_get_si( ((IntExpr*)code)->n ) << " );" << std::endl;
       indent( os, ind );
       os << incString.c_str() << std::endl;
     }
@@ -527,7 +527,7 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r
         indent( os, ind );
         os << "Expr* ";
         write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, os );
-        os << ";" << std::endl;
+        os << " = NULL;" << std::endl;
         std::ostringstream ss;
         write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, ss );
         write_code( ((CExpr*)code)->kids[1], os, ind, ss.str().c_str() );
@@ -841,7 +841,7 @@ void sccwriter::write_expr( Expr* code, std::ostream& os, int ind, std::string&
     {
       os << "static ";
     }
-    os << "Expr* " << ss.str().c_str() << ";" << std::endl;
+    os << "Expr* " << ss.str().c_str() << " = NULL;" << std::endl;
     //write the expression
     std::ostringstream ss2;
     ss2 << ss.str().c_str();
diff --git a/proofs/signatures/Makefile.am b/proofs/signatures/Makefile.am
index 2b6d16cfd..5947ad3f0 100644
--- a/proofs/signatures/Makefile.am
+++ b/proofs/signatures/Makefile.am
@@ -3,7 +3,8 @@
 # add support for more theories, just list them here in the same order
 # you would to the LFSC proof-checker binary.
 #
-CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_real.plf th_int.plf
+
+CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_bv_rewrites.plf th_real.plf th_int.plf
 
 noinst_LTLIBRARIES = libsignatures.la
 
diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf
index 5ed3d2f6f..b54a4ed5b 100755
--- a/proofs/signatures/th_arrays.plf
+++ b/proofs/signatures/th_arrays.plf
@@ -60,4 +60,4 @@
              (! u1 (! k (term s1)
                    (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k)))))
                      (holds cln)))
-               (holds cln)))))))
+               (holds cln)))))))
\ No newline at end of file
diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf
index c93541085..6012e052a 100644
--- a/proofs/signatures/th_bv.plf
+++ b/proofs/signatures/th_bv.plf
@@ -8,7 +8,7 @@
 
 (program mp_ispos ((x mpz)) formula
 	 (mp_ifneg x false true))
-	 
+
 (program mpz_eq ((x mpz) (y mpz)) formula
     (mp_ifzero (mpz_sub x y) true false))
 
@@ -21,7 +21,7 @@
 (program mpz_ ((x mpz) (y mpz)) formula
     (mp_ifzero (mpz_sub x y) true false))
 
-    
+
 ; "bitvec" is a term of type "sort"
 ; (declare BitVec sort)
 (declare BitVec (!n mpz sort))
@@ -37,7 +37,7 @@
 (declare bvc (! b bit (! v bv bv)))
 
 ; calculate the length of a bitvector
-;; (program bv_len ((v bv)) mpz 
+;; (program bv_len ((v bv)) mpz
 ;;   (match v
 ;;     (bvn 0)
 ;;     ((bvc b v') (mp_add (bv_len v') 1))))
@@ -48,7 +48,26 @@
 	 (! n mpz
 	 (! v bv
 	    (term (BitVec n)))))
-	 
+
+(program bv_constants_are_disequal ((x bv) (y bv)) formula
+  (match x
+      (bvn (fail formula))
+      ((bvc bx x')
+        (match y
+          (bvn (fail formula))
+          ((bvc by y') (match bx
+                             (b0 (match by (b0 (bv_constants_are_disequal x' y')) (b1 (true))))
+                             (b1 (match by (b0 (true)) (b1 (bv_constants_are_disequal x' y'))))
+          ))
+      ))
+))
+
+(declare bv_disequal_constants
+	 (! n mpz
+	 (! x bv
+	 (! y bv
+	 (! c (^ (bv_constants_are_disequal x y) true)
+  	   (th_holds (not (= (BitVec n) (a_bv n x) (a_bv n y)))))))))
 
 ; a bv variable
 (declare var_bv type)
@@ -61,7 +80,7 @@
 ; bit vector binary operators
 (define bvop2
 	(! n mpz
-	(! x (term (BitVec n)) 
+	(! x (term (BitVec n))
         (! y (term (BitVec n))
              	   (term (BitVec n))))))
 
@@ -88,7 +107,7 @@
 ; bit vector unary operators
 (define bvop1
 	(! n mpz
-	(! x (term (BitVec n)) 
+	(! x (term (BitVec n))
              	   (term (BitVec n)))))
 
 
@@ -111,8 +130,8 @@
 	 (! t1 (term (BitVec m))
 	 (! t2 (term (BitVec m'))
 	    (term (BitVec n))))))))
-	    
-;; side-condition fails in signature only??	    
+
+;; side-condition fails in signature only??
 ;;	 (! s (^ (mp_add m m') n)
 
 ;; (declare repeat bvopp)
@@ -147,22 +166,22 @@
 	    (term (BitVec n)))))))
 
 
-	   
-;; TODO: add checks for valid typing for these operators	   
+
+;; TODO: add checks for valid typing for these operators
 ;; (! c1 (^ (mpz_lte i j)
 ;; (! c2 (^ (mpz_lt i n) true)
 ;; (! c3 (^ (mp_ifneg i false true) true)
-;; (! c4 (^ (mp_ifneg j false true) true)	
+;; (! c4 (^ (mp_ifneg j false true) true)
 ;; (! s (^ (mp_add (mpz_sub i j) 1) m)
 
-	   
+
 ; bit vector predicates
 (define bvpred
 	(! n mpz
 	(! x (term (BitVec n))
 	(! y (term (BitVec n))
 	           formula))))
-		   
+
 (declare bvult bvpred)
 (declare bvule bvpred)
 (declare bvugt bvpred)
@@ -171,4 +190,3 @@
 (declare bvsle bvpred)
 (declare bvsgt bvpred)
 (declare bvsge bvpred)
-
diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf
index 8e8c51857..3cc1ec296 100644
--- a/proofs/signatures/th_bv_bitblast.plf
+++ b/proofs/signatures/th_bv_bitblast.plf
@@ -4,7 +4,7 @@
 (declare bbltc (! f formula (! v bblt bblt)))
 
 ; calculate the length of a bit-blasted term
-(program bblt_len ((v bblt)) mpz 
+(program bblt_len ((v bblt)) mpz
   (match v
     (bbltn 0)
     ((bbltc b v') (mp_add (bblt_len v') 1))))
@@ -25,6 +25,7 @@
 	    (bblast_term n x y)))))
 
 
+; Binds a symbol to the bblast_term to be used later on.
 (declare decl_bblast
 	 (! n mpz
 	 (! b bblt
@@ -34,6 +35,16 @@
 	 (! u (! v (bblast_term n t b) (holds cln))
 		   (holds cln))))))))
 
+(declare decl_bblast_with_alias
+	 (! n mpz
+	 (! b bblt
+	 (! t (term (BitVec n))
+	 (! a (term (BitVec n))
+	 (! bb (bblast_term n t b)
+	 (! e (th_holds (= _ t a))
+	 (! s (^ (bblt_len b) n)
+	 (! u (! v (bblast_term n a b) (holds cln))
+		   (holds cln))))))))))
 
 ; a predicate to represent the n^th bit of a bitvector term
 (declare bitof
@@ -46,31 +57,31 @@
 ;;           BITBLASTING RULES
 ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-	 
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST CONSTANT
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (program bblast_const ((v bv) (n mpz)) bblt
-  (mp_ifneg n (match v (bvn bbltn) 
+  (mp_ifneg n (match v (bvn bbltn)
                        (default (fail bblt)))
               (match v ((bvc b v') (bbltc (match b (b0 false) (b1 true)) (bblast_const v' (mp_add n (~ 1)))))
                        (default (fail bblt)))))
-              
+
 (declare bv_bbl_const (! n mpz
                       (! f bblt
                       (! v bv
                       (! c (^ (bblast_const v (mp_add n (~ 1))) f)
                            (bblast_term n (a_bv n v) f))))))
 
-		   
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST VARIABLE
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (program bblast_var ((x var_bv) (n mpz)) bblt
-  (mp_ifneg n bbltn 
+  (mp_ifneg n bbltn
               (bbltc (bitof x n) (bblast_var x (mp_add n (~ 1))))))
 
 (declare bv_bbl_var (! n mpz
@@ -79,18 +90,16 @@
                     (! c (^ (bblast_var x (mp_add n (~ 1))) f)
                          (bblast_term n (a_var_bv n x) f))))))
 
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST CONCAT
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (program bblast_concat ((x bblt) (y bblt)) bblt
-  (match x 
+  (match x
     (bbltn (match y ((bbltc by y') (bbltc by (bblast_concat x y')))
     	   	    (bbltn bbltn)))
     ((bbltc bx x') (bbltc bx (bblast_concat x' y)))))
-				
-				
+
 (declare bv_bbl_concat (! n mpz
 	 	       (! m mpz
 		       (! m1 mpz
@@ -104,36 +113,34 @@
                        (! c (^ (bblast_concat xb yb ) rb)
                            (bblast_term n (concat n m m1 x y) rb)))))))))))))
 
-			  
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST EXTRACT
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (program bblast_extract_rec ((x bblt) (i mpz) (j mpz) (n mpz)) bblt
-  (match x 
+  (match x
     ((bbltc bx x') (mp_ifneg (mpz_sub (mpz_sub j n) 1)
     	       	   	     (mp_ifneg (mpz_sub (mpz_sub n i) 1)
 			    	  	  (bbltc bx (bblast_extract_rec x' i j (mpz_sub n 1)))
 					  (bblast_extract_rec x' i j (mpz_sub n 1)))
- 					 
+
 			     bbltn))
    (bbltn bbltn)))
 
 (program bblast_extract ((x bblt) (i mpz) (j mpz) (n mpz)) bblt
- (bblast_extract_rec x i j (mpz_sub n 1)))			    
+ (bblast_extract_rec x i j (mpz_sub n 1)))
 
 (declare bv_bbl_extract (! n mpz
 			(! i mpz
 			(! j mpz
 			(! m mpz
-                       	(! x (term (BitVec m))	
+                       	(! x (term (BitVec m))
 		       	(! xb bblt
 		       	(! rb bblt
 		       	(! xbb (bblast_term m x xb)
 			(! c ( ^ (bblast_extract xb i j m) rb)
                            (bblast_term n (extract n i j m x) rb)))))))))))
 
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST ZERO/SIGN EXTEND
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -148,42 +155,38 @@
 (declare bv_bbl_zero_extend (! n mpz
 			(! k mpz
 			(! m mpz
-                       	(! x (term (BitVec m))	
+                       	(! x (term (BitVec m))
 		       	(! xb bblt
 		       	(! rb bblt
 		       	(! xbb (bblast_term m x xb)
 			(! c ( ^ (bblast_zextend xb k m) rb)
                            (bblast_term n (zero_extend n k m x) rb))))))))))
 
-			
 (program bblast_sextend ((x bblt) (i mpz)) bblt
  (match x (bbltn (fail bblt))
- 	  ((bbltc xb x') (extend_rec x (mpz_sub i 1) xb))))			    
+ 	  ((bbltc xb x') (extend_rec x (mpz_sub i 1) xb))))
 
 (declare bv_bbl_sign_extend (! n mpz
 			(! k mpz
 			(! m mpz
-                       	(! x (term (BitVec m))	
+                       	(! x (term (BitVec m))
 		       	(! xb bblt
 		       	(! rb bblt
 		       	(! xbb (bblast_term m x xb)
 			(! c ( ^ (bblast_sextend xb k m) rb)
                            (bblast_term n (sign_extend n k m x) rb))))))))))
-			   
-			   
-			     
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST BVAND
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-		 
+
 (program bblast_bvand ((x bblt) (y bblt)) bblt
-  (match x 
+  (match x
     (bbltn (match y (bbltn bbltn) (default (fail bblt))))
-    ((bbltc bx x') (match y 
+    ((bbltc bx x') (match y
                       (bbltn (fail bblt))
                       ((bbltc by y') (bbltc (and bx by) (bblast_bvand x' y')))))))
-				
-				
+
 (declare bv_bbl_bvand (! n mpz
                       (! x (term (BitVec n))
 		      (! y (term (BitVec n))
@@ -199,11 +202,10 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (program bblast_bvnot ((x bblt)) bblt
-  (match x 
-    (bbltn bbltn) 
+  (match x
+    (bbltn bbltn)
     ((bbltc bx x') (bbltc (not bx) (bblast_bvnot x')))))
-				
-				
+
 (declare bv_bbl_bvnot (! n mpz
                       (! x (term (BitVec n))
 		      (! xb bblt
@@ -215,15 +217,14 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST BVOR
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-			   
+
 (program bblast_bvor ((x bblt) (y bblt)) bblt
-  (match x 
+  (match x
     (bbltn (match y (bbltn bbltn) (default (fail bblt))))
-    ((bbltc bx x') (match y 
+    ((bbltc bx x') (match y
                       (bbltn (fail bblt))
                       ((bbltc by y') (bbltc (or bx by) (bblast_bvor x' y')))))))
-				
-				
+
 (declare bv_bbl_bvor (! n mpz
                       (! x (term (BitVec n))
 		      (! y (term (BitVec n))
@@ -238,15 +239,14 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST BVXOR
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-			   
+
 (program bblast_bvxor ((x bblt) (y bblt)) bblt
-  (match x 
+  (match x
     (bbltn (match y (bbltn bbltn) (default (fail bblt))))
-    ((bbltc bx x') (match y 
+    ((bbltc bx x') (match y
                       (bbltn (fail bblt))
                       ((bbltc by y') (bbltc (xor bx by) (bblast_bvxor x' y')))))))
-				
-				
+
 (declare bv_bbl_bvxor (! n mpz
                       (! x (term (BitVec n))
 		      (! y (term (BitVec n))
@@ -262,8 +262,8 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST BVADD
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-			   
-;; return the carry bit after adding x y			   
+
+;; return the carry bit after adding x y
 ;; FIXME: not the most efficient thing in the world
 (program bblast_bvadd_carry ((a bblt) (b bblt) (carry formula)) formula
 (match a
@@ -272,7 +272,7 @@
   	     	   (bbltn (fail formula))
 	 	   ((bbltc bi b') (or (and ai bi) (and (xor ai bi) (bblast_bvadd_carry a' b' carry))))))))
 
-;; ripple carry adder where carry is the initial carry bit		   
+;; ripple carry adder where carry is the initial carry bit
 (program bblast_bvadd ((a bblt) (b bblt) (carry formula)) bblt
 (match a
   ( bbltn (match b (bbltn bbltn) (default (fail bblt))))
@@ -280,8 +280,35 @@
   	     	   (bbltn (fail bblt))
 	 	   ((bbltc bi b') (bbltc (xor (xor ai bi) (bblast_bvadd_carry a' b' carry))
 				  	 (bblast_bvadd a' b' carry)))))))
-				
-				
+
+
+(program reverse_help ((x bblt) (acc bblt)) bblt
+(match x
+       (bbltn acc)
+       ((bbltc xi x') (reverse_help x' (bbltc xi acc)))))
+
+
+(program reverseb ((x bblt)) bblt
+	 (reverse_help x bbltn))
+
+
+; AJR: use this version?
+;(program bblast_bvadd_2h ((a bblt) (b bblt) (carry formula)) bblt
+;(match a
+;  ( bbltn (match b (bbltn bbltn) (default (fail bblt))))
+;  ((bbltc ai a') (match b
+;       (bbltn (fail bblt))
+;	 	   ((bbltc bi b')
+;	 	     (let carry' (or (and ai bi) (and (xor ai bi) carry))
+;	 	     (bbltc (xor (xor ai bi) carry)
+;				  	    (bblast_bvadd_2h a' b' carry'))))))))
+
+;(program bblast_bvadd_2 ((a bblt) (b bblt) (carry formula)) bblt
+;(let ar (reverseb a) ;; reverse a and b so that we can build the circuit
+;(let br (reverseb b) ;; from the least significant bit up
+;(let ret (bblast_bvadd_2h ar br carry)
+;  (reverseb ret)))))
+
 (declare bv_bbl_bvadd (! n mpz
                       (! x (term (BitVec n))
 		      (! y (term (BitVec n))
@@ -293,7 +320,6 @@
                       (! c (^ (bblast_bvadd xb yb false) rb)
                            (bblast_term n (bvadd n x y) rb)))))))))))
 
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST BVNEG
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -304,8 +330,8 @@
 
 (program bblast_bvneg ((x bblt) (n mpz)) bblt
   (bblast_bvadd (bblast_bvnot x) (bblast_zero n) true))
-				
-				
+
+
 (declare bv_bbl_bvneg (! n mpz
                       (! x (term (BitVec n))
 		      (! xb bblt
@@ -319,23 +345,14 @@
 ;; BITBLAST BVMUL
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-			   
-;; shift add multiplier
-
-(program reverse_help ((x bblt) (acc bblt)) bblt
-(match x
-       (bbltn acc)
-       ((bbltc xi x') (reverse_help x' (bbltc xi acc)))))
-
 
-(program reverseb ((x bblt)) bblt
-	 (reverse_help x bbltn))
+;; shift add multiplier
 
 ;; (program concat ((a bblt) (b bblt)) bblt
 ;;   (match a (bbltn b)
 ;;   	   ((bbltc ai a') (bbltc ai (concat a' b)))))
 
-	   
+
 (program top_k_bits ((a bblt) (k mpz)) bblt
   (mp_ifzero k bbltn
   	     (match a (bbltn (fail bblt))
@@ -344,7 +361,7 @@
 (program bottom_k_bits ((a bblt) (k mpz)) bblt
  (reverseb (top_k_bits (reverseb a) k)))
 
-;; assumes the least signigicant bit is at the beginning of the list 
+;; assumes the least signigicant bit is at the beginning of the list
 (program k_bit ((a bblt) (k mpz)) formula
 (mp_ifneg k (fail formula)
 (match a (bbltn (fail formula))
@@ -353,7 +370,7 @@
 (program and_with_bit ((a bblt) (bt formula)) bblt
 (match a (bbltn bbltn)
          ((bbltc ai a') (bbltc (and bt ai) (and_with_bit a' bt)))))
-	 
+
 ;; a is going to be the current result
 ;; carry is going to be false initially
 ;; b is the and of a and b[k]
@@ -377,19 +394,19 @@
 (let ak (top_k_bits a k')
 (let b' (and_with_bit ak (k_bit b k))
  (mp_ifzero (mpz_sub k' 1)
-   (mult_step_k_h res b' bbltn false k)	
+   (mult_step_k_h res b' bbltn false k)
    (let res' (mult_step_k_h res b' bbltn false k)
    (mult_step a b (reverseb res') n (mp_add k 1))))))))
 
 
 (program bblast_bvmul ((a bblt) (b bblt) (n mpz)) bblt
-(let ar (reverseb a) ;; reverse a and b so that we can build the circuit 
+(let ar (reverseb a) ;; reverse a and b so that we can build the circuit
 (let br (reverseb b) ;; from the least significant bit up
 (let res (and_with_bit ar (k_bit br 0))
-     (mp_ifzero (mpz_sub n 1)     ;; if multiplying 1 bit numbers no need to call mult_step 
+     (mp_ifzero (mpz_sub n 1)     ;; if multiplying 1 bit numbers no need to call mult_step
      		res
 		(mult_step ar br res n 1))))))
-     
+
 (declare bv_bbl_bvmul (! n mpz
                       (! x (term (BitVec n))
 		      (! y (term (BitVec n))
@@ -402,18 +419,18 @@
                            (bblast_term n (bvmul n x y) rb)))))))))))
 
 
-			   
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST EQUALS
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-			   
+
 ; bit blast  x = y
 ; for x,y of size n, it will return a conjuction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1})))
 ; f is the accumulator formula that builds the equality in the right order
 (program bblast_eq_rec ((x bblt) (y bblt) (f formula)) formula
-  (match x 
+  (match x
     (bbltn (match y (bbltn f) (default (fail formula))))
-    ((bbltc fx x') (match y 
+    ((bbltc fx x') (match y
                       (bbltn (fail formula))
                       ((bbltc fy y') (bblast_eq_rec x' y' (and (iff fx fy) f)))))
     (default (fail formula))))
@@ -423,7 +440,23 @@
 	 	((bbltc bx x') (match y ((bbltc by y') (bblast_eq_rec x' y' (iff bx by)))
 			       	      	(default (fail formula))))
 		(default (fail formula))))
-	
+
+
+;; TODO: a temporary bypass for rewrites that we don't support yet. As soon
+;; as we do, remove this rule.
+
+(declare bv_bbl_=_false
+	 (! n mpz
+	 (! x (term (BitVec n))
+         (! y (term (BitVec n))
+         (! bx bblt
+         (! by bblt
+         (! f formula
+         (! bbx (bblast_term n x bx)
+         (! bby (bblast_term n y by)
+         (! c (^ (bblast_eq bx by) f)
+            (th_holds (iff (= (BitVec n) x y) false))))))))))))
+
 (declare bv_bbl_=
 	 (! n mpz
 	 (! x (term (BitVec n))
@@ -436,11 +469,22 @@
          (! c (^ (bblast_eq bx by) f)
             (th_holds (iff (= (BitVec n) x y) f))))))))))))
 
-			 
+(declare bv_bbl_=_swap
+	 (! n mpz
+	 (! x (term (BitVec n))
+         (! y (term (BitVec n))
+         (! bx bblt
+         (! by bblt
+         (! f formula
+         (! bbx (bblast_term n x bx)
+         (! bby (bblast_term n y by)
+         (! c (^ (bblast_eq by bx) f)
+            (th_holds (iff (= (BitVec n) x y) f))))))))))))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST BVULT
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-	    
+
 (program bblast_bvult ((x bblt) (y bblt) (n mpz)) formula
 (match x
   ( bbltn (fail formula))
@@ -465,7 +509,7 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST BVSLT
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-	    
+
 (program bblast_bvslt ((x bblt) (y bblt) (n mpz)) formula
 (match x
   ( bbltn (fail formula))
@@ -488,7 +532,6 @@
          (! bby (bblast_term n y by)
          (! c (^ (bblast_bvslt bx by n) f)
             (th_holds (iff (bvslt n x y) f))))))))))))
-	    
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -525,8 +568,8 @@
 ;;           REWRITE RULES
 ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-	    
-	    
+
+
 ; rewrite rule :
 ; x + y = y + x
 (declare bvadd_symm
@@ -534,7 +577,7 @@
 	 (! x (term (BitVec n))
 	 (! y (term (BitVec n))
 	    (th_holds (= (BitVec n) (bvadd _ x y) (bvadd _ y x)))))))
-	    
+
 ;; (declare bvcrazy_rewrite
 ;; 	 (! n mpz
 ;; 	 (! x (term (BitVec n))
@@ -546,12 +589,12 @@
 ;; 	 (! s (^ (rewrite_scc xn yn) true)
 ;; 	 (! u (! x (term (BitVec n)) (holds cln))
 ;; 	     (holds cln)))))))))))
-	 
+
 ;; 	    (th_holds (= (BitVec n) (bvadd x y) (bvadd y x)))))))
 
-	    
-	    
-; necessary? 
+
+
+; necessary?
 ;; (program calc_bvand ((a bv) (b bv)) bv
 ;;   (match a
 ;;     (bvn (match b (bvn bvn) (default (fail bv))))
@@ -560,7 +603,7 @@
 ;;                       (default (fail bv))))))
 
 ;; ; rewrite rule (w constants) :
-;; ; a & b = c    
+;; ; a & b = c
 ;; (declare bvand_const (! c bv
 ;; 		     (! a bv
 ;;                      (! b bv
@@ -568,7 +611,7 @@
 ;;                         (th_holds (= BitVec (bvand (a_bv a) (a_bv b)) (a_bv c))))))))
 
 
-;; making constant bit-vectors	 
+;; making constant bit-vectors
 (program mk_ones ((n mpz)) bv
 	(mp_ifzero n bvn (bvc b1 (mk_ones (mpz_sub n 1)))))
 
@@ -576,7 +619,7 @@
 	(mp_ifzero n bvn (bvc b0 (mk_ones (mpz_sub n 1)))))
 
 
-	
+
 ;; (bvxnor a b) => (bvnot (bvxor a b))
 ;; (declare bvxnor_elim
 ;; 	 (! n mpz
@@ -603,7 +646,7 @@
 ;; 	 (! rwb (rw_term _ b (a_bv _ zero_bits))
 ;; 	 (rw_term _  (bvxor _ a b)
 ;; 	 	  a'))))))))))
-		  
+
 ;; ;; (bvxor a 11) => (bvnot a)
 ;; (declare bvxor_one
 ;; 	 (! n mpz
@@ -617,7 +660,7 @@
 ;; 	 (rw_term _ (bvxor _ a b)
 ;; 	 	  (bvnot _ a')))))))))))
 
-		  
+
 ;; ;; (bvnot (bvnot a)) => a
 ;; (declare bvnot_idemp
 ;; 	 (! n mpz
@@ -626,4 +669,3 @@
 ;; 	 (! rwa (rw_term _  a a')
 ;; 	 (rw_term _ (bvnot _ (bvnot _ a))
 ;; 	 	  a'))))))
-
diff --git a/proofs/signatures/th_bv_rewrites.plf b/proofs/signatures/th_bv_rewrites.plf
new file mode 100644
index 000000000..bf5dea9e9
--- /dev/null
+++ b/proofs/signatures/th_bv_rewrites.plf
@@ -0,0 +1,22 @@
+;
+; Equality swap
+;
+
+(declare rr_bv_eq
+	 (! n mpz
+	 (! t1 (term (BitVec n))
+ 	 (! t2 (term (BitVec n))
+	     (th_holds (iff (= (BitVec n) t2 t1) (= (BitVec n) t1 t2)))))))
+
+;
+; Additional rules...
+;
+
+;
+; Default, if nothing else applied
+;
+
+(declare rr_bv_default
+	 (! t1 formula
+ 	 (! t2 formula
+	     (th_holds (iff t1 t2))))))
diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf
index d85b2115c..e212f835d 100755
--- a/proofs/signatures/th_quant.plf
+++ b/proofs/signatures/th_quant.plf
@@ -14,10 +14,7 @@
       (match ti
         ((apply si1 si2 ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
         (default ff)))
-    (default
-      (match ti
-        ((apply si1 si2 ti1 ti2) ff)
-        (default (eqterm ti (ifmarked t k t)))))))
+    (default (eqterm ti (ifmarked t k t)))))
 
 (program is_inst_f ((fi formula) (f formula) (k term)) bool
   (match f