Cegqi bv remove extract terms preprocess pass (#1376)

* Preprocess extract -> concat pass for cegqi bv.

* Add sygus bench

* Fixes, infrastructure.

* Minor fixes.

* Try

* Minor

* Minor

* Document

* Format

* Improving debug messages.

* Address

* Format

* Overlapping extracts.

* Format

* Minor

* Address review.

* Format

* Comment

* Format

8 files changed, 468 insertions, 139 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index c6dbe60c7..8106c5e5d 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -343,6 +343,8 @@ option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :defaul
   interleave model value instantiation with word-level inversion approach
 option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqMode :read-write :default CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_SLACK :include "options/quantifiers_modes.h" :handler stringToCbqiBvIneqMode
  choose mode for handling bit-vector inequalities with counterexample-guided instantiation
+option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default false 
+  replaces extract terms with variables for counterexample-guided instantiation for bit-vectors
  
 ### local theory extensions options 
 
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index b41a3cfca..15bfbe9f9 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -33,6 +33,33 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+std::ostream& operator<<(std::ostream& os, CegInstEffort e)
+{
+  switch (e)
+  {
+    case CEG_INST_EFFORT_NONE: os << "?"; break;
+    case CEG_INST_EFFORT_STANDARD: os << "STANDARD"; break;
+    case CEG_INST_EFFORT_STANDARD_MV: os << "STANDARD_MV"; break;
+    case CEG_INST_EFFORT_FULL: os << "FULL"; break;
+    default: Unreachable();
+  }
+  return os;
+}
+
+std::ostream& operator<<(std::ostream& os, CegInstPhase phase)
+{
+  switch (phase)
+  {
+    case CEG_INST_PHASE_NONE: os << "?"; break;
+    case CEG_INST_PHASE_EQC: os << "eqc"; break;
+    case CEG_INST_PHASE_EQUAL: os << "eq"; break;
+    case CEG_INST_PHASE_ASSERTION: os << "as"; break;
+    case CEG_INST_PHASE_MVALUE: os << "mv"; break;
+    default: Unreachable();
+  }
+  return os;
+}
+
 CegInstantiator::CegInstantiator(QuantifiersEngine* qe,
                                  CegqiOutput* out,
                                  bool use_vts_delta,
@@ -41,9 +68,8 @@ CegInstantiator::CegInstantiator(QuantifiersEngine* qe,
       d_out(out),
       d_use_vts_delta(use_vts_delta),
       d_use_vts_inf(use_vts_inf),
-      d_num_input_variables(0),
       d_is_nested_quant(false),
-      d_effort(INST_EFFORT_NONE)
+      d_effort(CEG_INST_EFFORT_NONE)
 {
 }
 
@@ -129,6 +155,7 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index)
   }
   d_curr_subs_proc[v].clear();
   d_curr_index[v] = index;
+  d_curr_iphase[v] = CEG_INST_PHASE_NONE;
 }
 
 void CegInstantiator::registerTheoryIds(TypeNode tn,
@@ -161,7 +188,10 @@ void CegInstantiator::registerTheoryId(TheoryId tid)
   if (std::find(d_tids.begin(), d_tids.end(), tid) == d_tids.end())
   {
     // setup any theory-specific preprocessors here
-
+    if (tid == THEORY_BV)
+    {
+      d_tipp[tid] = new BvInstantiatorPreprocess;
+    }
     d_tids.push_back(tid);
   }
 }
@@ -192,6 +222,7 @@ void CegInstantiator::deactivateInstantiationVariable(Node v)
 {
   d_curr_subs_proc.erase( v );
   d_curr_index.erase( v );
+  d_curr_iphase.erase(v);
 }
 
 bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
@@ -199,7 +230,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
   if( i==d_vars.size() ){
     //solved for all variables, now construct instantiation
     bool needsPostprocess =
-        sf.d_vars.size() > d_num_input_variables || !d_var_order_index.empty();
+        sf.d_vars.size() > d_input_vars.size() || !d_var_order_index.empty();
     std::vector< Instantiator * > pp_inst;
     std::map< Instantiator *, Node > pp_inst_to_var;
     std::vector< Node > lemmas;
@@ -268,10 +299,11 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
     }
 
     // if d_effort is full, we must choose at least one model value
-    if ((i + 1) < d_vars.size() || d_effort != INST_EFFORT_FULL)
+    if ((i + 1) < d_vars.size() || d_effort != CEG_INST_EFFORT_FULL)
     {
       //[1] easy case : pv is in the equivalence class as another term not containing pv
       Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl;
+      d_curr_iphase[pv] = CEG_INST_PHASE_EQC;
       std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr );
       if( it_eqc!=d_curr_eqc.end() ){
         //std::vector< Node > eq_candidates;
@@ -320,6 +352,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
       if (vinst->hasProcessEquality(this, sf, pv, d_effort))
       {
         Trace("cbqi-inst-debug") << "[2] try based on solving equalities." << std::endl;
+        d_curr_iphase[pv] = CEG_INST_PHASE_EQUAL;
         for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){
           Node r = d_curr_type_eqc[pvtnb][k];
           std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r );
@@ -381,6 +414,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
       if (vinst->hasProcessAssertion(this, sf, pv, d_effort))
       {
         Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl;
+        d_curr_iphase[pv] = CEG_INST_PHASE_ASSERTION;
         std::unordered_set< Node, NodeHashFunction > lits;
         //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
         for( unsigned r=0; r<2; r++ ){
@@ -426,11 +460,11 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
     }
 
     //[4] resort to using value in model. We do so if:
-    // - we are in a higher effort than INST_EFFORT_STANDARD,
+    // - we are in a higher effort than CEG_INST_EFFORT_STANDARD,
     // - if the variable is Boolean, or
     // - if we are solving for a subfield of a datatype.
     bool use_model_value = vinst->useModelValue(this, sf, pv, d_effort);
-    if ((d_effort > INST_EFFORT_STANDARD || use_model_value || is_cv)
+    if ((d_effort > CEG_INST_EFFORT_STANDARD || use_model_value || is_cv)
         && vinst->allowModelValue(this, sf, pv, d_effort))
     {
 #ifdef CVC4_ASSERTIONS
@@ -442,11 +476,12 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
       Node mv = getModelValue( pv );
       TermProperties pv_prop_m;
       Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
-      InstEffort prev = d_effort;
+      d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE;
+      CegInstEffort prev = d_effort;
       if (!use_model_value)
       {
         // update the effort level to indicate we have used a model value
-        d_effort = INST_EFFORT_STANDARD_MV;
+        d_effort = CEG_INST_EFFORT_STANDARD_MV;
       }
       if (constructInstantiationInc(pv, mv, pv_prop_m, sf))
       {
@@ -482,13 +517,14 @@ bool CegInstantiator::constructInstantiationInc(Node pv,
   Node cnode = pv_prop.getCacheNode();
   if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){
     d_curr_subs_proc[pv][n][cnode] = true;
-    if( Trace.isOn("cbqi-inst") ){
+    if( Trace.isOn("cbqi-inst-debug") ){
       for( unsigned j=0; j<sf.d_subs.size(); j++ ){
-        Trace("cbqi-inst") << " ";
+        Trace("cbqi-inst-debug") << " ";
       }
-      Trace("cbqi-inst") << sf.d_subs.size() << ": ";
+      Trace("cbqi-inst-debug") << sf.d_subs.size() << ": (" << d_curr_iphase[pv]
+                         << ") ";
       Node mod_pv = pv_prop.getModifiedTerm( pv );
-      Trace("cbqi-inst") << mod_pv << " -> " << n << std::endl;
+      Trace("cbqi-inst-debug") << mod_pv << " -> " << n << std::endl;
       Assert( n.getType().isSubtypeOf( pv.getType() ) );
     }
     //must ensure variables have been computed for n
@@ -599,7 +635,7 @@ bool CegInstantiator::constructInstantiationInc(Node pv,
 }
 
 bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ) {
-  if (vars.size() > d_num_input_variables)
+  if (vars.size() > d_input_vars.size() || !d_var_order_index.empty())
   {
     Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl;
     std::map< Node, Node > subs_map;
@@ -607,26 +643,28 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector
       subs_map[vars[i]] = subs[i];
     }
     subs.clear();
-    for (unsigned i = 0; i < d_vars.size(); i++)
+    for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i)
     {
-      std::map< Node, Node >::iterator it = subs_map.find( d_vars[i] );
+      std::map<Node, Node>::iterator it = subs_map.find(d_input_vars[i]);
       Assert( it!=subs_map.end() );
       Node n = it->second;
-      Trace("cbqi-inst-debug") << "  " << d_vars[i] << " -> " << n << std::endl;
+      Trace("cbqi-inst-debug") << "  " << d_input_vars[i] << " -> " << n
+                               << std::endl;
+      Assert(n.getType().isSubtypeOf(d_input_vars[i].getType()));
       subs.push_back( n );
     }
   }
-  Trace("cbqi-inst-debug") << "Sort based on order...." << std::endl;
-  if( !d_var_order_index.empty() ){
-    std::vector< Node > subs_orig;
-    subs_orig.insert( subs_orig.end(), subs.begin(), subs.end() );
-    subs.clear();
-    for( unsigned i=0; i<subs_orig.size(); i++ ){
-      Assert(d_var_order_index[i]<subs_orig.size());
-      subs.push_back( subs_orig[d_var_order_index[i]] );
+  if (Trace.isOn("cbqi-inst"))
+  {
+    Trace("cbqi-inst") << "Ceg Instantiator produced : " << std::endl;
+    for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i)
+    {
+      Node v = d_input_vars[i];
+      Trace("cbqi-inst") << i << " (" << d_curr_iphase[v] << ") : " 
+                         << v << " -> " << subs[i] << std::endl;
+      Assert(subs[i].getType().isSubtypeOf(v.getType()));
     }
   }
-  subs.resize(d_num_input_variables);
   Trace("cbqi-inst-debug") << "Do the instantiation...." << std::endl;
   bool ret = d_out->doAddInstantiation( subs );
   for( unsigned i=0; i<lemmas.size(); i++ ){
@@ -818,7 +856,7 @@ bool CegInstantiator::check() {
   }
   processAssertions();
   for( unsigned r=0; r<2; r++ ){
-    d_effort = r == 0 ? INST_EFFORT_STANDARD : INST_EFFORT_FULL;
+    d_effort = r == 0 ? CEG_INST_EFFORT_STANDARD : CEG_INST_EFFORT_FULL;
     SolvedForm sf;
     d_stack_vars.clear();
     d_bound_var_index.clear();
@@ -1133,9 +1171,11 @@ struct sortCegVarOrder {
 
 void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
   Trace("cbqi-reg") << "Register counterexample lemma..." << std::endl;
+  d_input_vars.clear();
+  d_input_vars.insert(d_input_vars.end(), ce_vars.begin(), ce_vars.end());
+
   //Assert( d_vars.empty() );
   d_vars.clear();
-  d_num_input_variables = ce_vars.size();
   registerTheoryId(THEORY_UF);
   for (unsigned i = 0; i < ce_vars.size(); i++)
   {
@@ -1143,6 +1183,26 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
     registerVariable(ce_vars[i]);
   }
 
+  // preprocess with all relevant instantiator preprocessors
+  Trace("cbqi-debug") << "Preprocess based on theory-specific methods..."
+                      << std::endl;
+  std::vector<Node> pvars;
+  pvars.insert(pvars.end(), d_vars.begin(), d_vars.end());
+  for (std::pair<const TheoryId, InstantiatorPreprocess*>& p : d_tipp)
+  {
+    p.second->registerCounterexampleLemma(lems, pvars);
+  }
+  // must register variables generated by preprocessors
+  Trace("cbqi-debug") << "Register variables from theory-specific methods "
+                      << d_input_vars.size() << " " << pvars.size() << " ..."
+                      << std::endl;
+  for (unsigned i = d_input_vars.size(), size = pvars.size(); i < size; ++i)
+  {
+    Trace("cbqi-reg") << "  register theory preprocess variable : " << pvars[i]
+                      << std::endl;
+    registerVariable(pvars[i]);
+  }
+
   //remove ITEs
   IteSkolemMap iteSkolemMap;
   d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap);
@@ -1181,28 +1241,6 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
     lems[i] = rlem;
   }
 
-  // preprocess with all relevant instantiator preprocessors
-  Trace("cbqi-debug") << "Preprocess based on theory-specific methods..."
-                      << std::endl;
-  std::vector<Node> pvars;
-  pvars.insert(pvars.end(), d_vars.begin(), d_vars.end());
-  for (std::map<TheoryId, InstantiatorPreprocess*>::iterator it =
-           d_tipp.begin();
-       it != d_tipp.end();
-       ++it)
-  {
-    it->second->registerCounterexampleLemma(lems, pvars);
-  }
-  // must register variables generated by preprocessors
-  Trace("cbqi-debug") << "Register variables from theory-specific methods "
-                      << d_num_input_variables << " " << d_vars.size() << " ..."
-                      << std::endl;
-  for (unsigned i = d_num_input_variables; i < pvars.size(); i++)
-  {
-    Trace("cbqi-reg") << "  register theory preprocess variable : " << pvars[i] << std::endl;
-    registerVariable(pvars[i]);
-  }
-
   // determine variable order: must do Reals before Ints
   Trace("cbqi-debug") << "Determine variable order..." << std::endl;
   if (!d_vars.empty())
@@ -1257,7 +1295,7 @@ bool Instantiator::processEqualTerm(CegInstantiator* ci,
                                     Node pv,
                                     TermProperties& pv_prop,
                                     Node n,
-                                    InstEffort effort)
+                                    CegInstEffort effort)
 {
   pv_prop.d_type = 0;
   return ci->constructInstantiationInc(pv, n, pv_prop, sf);
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index bf5a37026..ab9c7ea05 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__CEG_INSTANTIATOR_H
-#define __CVC4__CEG_INSTANTIATOR_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
+#define __CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
 
 #include "theory/quantifiers_engine.h"
 #include "util/statistics_registry.h"
@@ -143,19 +143,47 @@ public:
   }
 };
 
-/** instantiation effort levels */
-enum InstEffort
+/** instantiation effort levels
+ *
+ * This effort is used to stratify the construction of
+ * instantiations for some theories that may result to
+ * using model value instantiations.
+ */
+enum CegInstEffort
 {
   // uninitialized
-  INST_EFFORT_NONE,
+  CEG_INST_EFFORT_NONE,
   // standard effort level
-  INST_EFFORT_STANDARD,
+  CEG_INST_EFFORT_STANDARD,
   // standard effort level, but we have used model values
-  INST_EFFORT_STANDARD_MV,
+  CEG_INST_EFFORT_STANDARD_MV,
   // full effort level
-  INST_EFFORT_FULL
+  CEG_INST_EFFORT_FULL
+};
+
+std::ostream& operator<<(std::ostream& os, CegInstEffort e);
+
+/** instantiation phase for variables
+ *
+ * This indicates the phase in which we constructed
+ * a substitution for individual variables.
+ */
+enum CegInstPhase
+{
+  // uninitialized
+  CEG_INST_PHASE_NONE,
+  // instantiation constructed during traversal of equivalence classes
+  CEG_INST_PHASE_EQC,
+  // instantiation constructed during solving equalities
+  CEG_INST_PHASE_EQUAL,
+  // instantiation constructed by looking at theory assertions
+  CEG_INST_PHASE_ASSERTION,
+  // instantiation constructed by querying model value
+  CEG_INST_PHASE_MVALUE,
 };
 
+std::ostream& operator<<(std::ostream& os, CegInstPhase phase);
+
 /** Ceg instantiator
  *
  * This class manages counterexample-guided quantifier instantiation
@@ -357,9 +385,9 @@ class CegInstantiator {
 
   //-------------------------------the variables
   /** the variables we are instantiating
-   * For a quantified formula with n variables,
-   * the first n terms in d_vars are the instantiation
-   * constants corresponding to these variables.
+   *
+   * This is a superset of the variables for the instantiations we are
+   * generating and sending on the output channel of this class.
    */
   std::vector<Node> d_vars;
   /** set form of d_vars */
@@ -367,10 +395,11 @@ class CegInstantiator {
   /** index of variables reported in instantiation */
   std::vector<unsigned> d_var_order_index;
   /** number of input variables
-   * This is n for quantified formulas with n variables,
-   * and is at most the size of d_vars.
+   *
+   * These are the variables, in order, for the instantiations we are generating
+   * and sending on the output channel of this class.
    */
-  unsigned d_num_input_variables;
+  std::vector<Node> d_input_vars;
   /** literals to equalities for aux vars
    * This stores entries of the form
    *   L -> ( k -> t )
@@ -416,13 +445,15 @@ class CegInstantiator {
    * This indicates the effort Instantiator objects
    * will put into the terms they return.
    */
-  InstEffort d_effort;
+  CegInstEffort d_effort;
   /** for each variable, the instantiator used for that variable */
   std::map<Node, Instantiator*> d_active_instantiators;
   /** map from variables to the index in the prefix of the quantified
    * formula we are processing.
    */
   std::map<Node, unsigned> d_curr_index;
+  /** map from variables to the phase in which we instantiated them */
+  std::map<Node, CegInstPhase> d_curr_iphase;
   /** cache of current substitutions tried between activate/deactivate */
   std::map<Node, std::map<Node, std::map<Node, bool> > > d_curr_subs_proc;
   /** stack of temporary variables we are solving for,
@@ -520,7 +551,7 @@ public:
   virtual void reset(CegInstantiator* ci,
                      SolvedForm& sf,
                      Node pv,
-                     InstEffort effort)
+                     CegInstEffort effort)
   {
   }
 
@@ -538,7 +569,7 @@ public:
                                 Node pv,
                                 TermProperties& pv_prop,
                                 Node n,
-                                InstEffort effort);
+                                CegInstEffort effort);
   /** process equal terms
    *
    * This method is called after process equal term, where eqc is the list of
@@ -551,7 +582,7 @@ public:
                                  SolvedForm& sf,
                                  Node pv,
                                  std::vector<Node>& eqc,
-                                 InstEffort effort)
+                                 CegInstEffort effort)
   {
     return false;
   }
@@ -560,7 +591,7 @@ public:
   virtual bool hasProcessEquality(CegInstantiator* ci,
                                   SolvedForm& sf,
                                   Node pv,
-                                  InstEffort effort)
+                                  CegInstEffort effort)
   {
     return false;
   }
@@ -581,7 +612,7 @@ public:
                                Node pv,
                                std::vector<TermProperties>& term_props,
                                std::vector<Node>& terms,
-                               InstEffort effort)
+                               CegInstEffort effort)
   {
     return false;
   }
@@ -590,7 +621,7 @@ public:
   virtual bool hasProcessAssertion(CegInstantiator* ci,
                                    SolvedForm& sf,
                                    Node pv,
-                                   InstEffort effort)
+                                   CegInstEffort effort)
   {
     return false;
   }
@@ -609,8 +640,11 @@ public:
   *   (2) lit' implies lit.
   *   where typically lit' = lit.
   */
-  virtual Node hasProcessAssertion(
-      CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, InstEffort effort)
+  virtual Node hasProcessAssertion(CegInstantiator* ci,
+                                   SolvedForm& sf,
+                                   Node pv,
+                                   Node lit,
+                                   CegInstEffort effort)
   {
     return Node::null();
   }
@@ -628,7 +662,7 @@ public:
                                 Node pv,
                                 Node lit,
                                 Node alit,
-                                InstEffort effort)
+                                CegInstEffort effort)
   {
     return false;
   }
@@ -643,7 +677,7 @@ public:
   virtual bool processAssertions(CegInstantiator* ci,
                                  SolvedForm& sf,
                                  Node pv,
-                                 InstEffort effort)
+                                 CegInstEffort effort)
   {
     return false;
   }
@@ -655,7 +689,7 @@ public:
   virtual bool useModelValue(CegInstantiator* ci,
                              SolvedForm& sf,
                              Node pv,
-                             InstEffort effort)
+                             CegInstEffort effort)
   {
     return false;
   }
@@ -663,7 +697,7 @@ public:
   virtual bool allowModelValue(CegInstantiator* ci,
                                SolvedForm& sf,
                                Node pv,
-                               InstEffort effort)
+                               CegInstEffort effort)
   {
     return d_closed_enum_type;
   }
@@ -672,7 +706,7 @@ public:
   virtual bool needsPostProcessInstantiationForVariable(CegInstantiator* ci,
                                                         SolvedForm& sf,
                                                         Node pv,
-                                                        InstEffort effort)
+                                                        CegInstEffort effort)
   {
     return false;
   }
@@ -684,7 +718,7 @@ public:
   virtual bool postProcessInstantiationForVariable(CegInstantiator* ci,
                                                    SolvedForm& sf,
                                                    Node pv,
-                                                   InstEffort effort,
+                                                   CegInstEffort effort,
                                                    std::vector<Node>& lemmas)
   {
     return true;
@@ -706,7 +740,7 @@ public:
   bool useModelValue(CegInstantiator* ci,
                      SolvedForm& sf,
                      Node pv,
-                     InstEffort effort)
+                     CegInstEffort effort)
   {
     return true;
   }
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index d58fa2f1e..674f7c17e 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -219,7 +219,7 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No
 void ArithInstantiator::reset(CegInstantiator* ci,
                               SolvedForm& sf,
                               Node pv,
-                              InstEffort effort)
+                              CegInstEffort effort)
 {
   d_vts_sym[0] = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type, false, false );
   d_vts_sym[1] = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta( false, false );
@@ -238,7 +238,7 @@ bool ArithInstantiator::processEquality(CegInstantiator* ci,
                                         Node pv,
                                         std::vector<TermProperties>& term_props,
                                         std::vector<Node>& terms,
-                                        InstEffort effort)
+                                        CegInstEffort effort)
 {
   Node eq_lhs = terms[0];
   Node eq_rhs = terms[1];
@@ -276,8 +276,11 @@ bool ArithInstantiator::processEquality(CegInstantiator* ci,
   return false;
 }
 
-Node ArithInstantiator::hasProcessAssertion(
-    CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, InstEffort effort)
+Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci,
+                                            SolvedForm& sf,
+                                            Node pv,
+                                            Node lit,
+                                            CegInstEffort effort)
 {
   Node atom = lit.getKind()==NOT ? lit[0] : lit;
   bool pol = lit.getKind()!=NOT;
@@ -295,7 +298,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
                                          Node pv,
                                          Node lit,
                                          Node alit,
-                                         InstEffort effort)
+                                         CegInstEffort effort)
 {
   Node atom = lit.getKind()==NOT ? lit[0] : lit;
   bool pol = lit.getKind()!=NOT;
@@ -415,7 +418,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
 bool ArithInstantiator::processAssertions(CegInstantiator* ci,
                                           SolvedForm& sf,
                                           Node pv,
-                                          InstEffort effort)
+                                          CegInstEffort effort)
 {
   if (options::cbqiModel()) {
     bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() );
@@ -637,7 +640,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
 }
 
 bool ArithInstantiator::needsPostProcessInstantiationForVariable(
-    CegInstantiator* ci, SolvedForm& sf, Node pv, InstEffort effort)
+    CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort)
 {
   return std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end();
 }
@@ -646,7 +649,7 @@ bool ArithInstantiator::postProcessInstantiationForVariable(
     CegInstantiator* ci,
     SolvedForm& sf,
     Node pv,
-    InstEffort effort,
+    CegInstEffort effort,
     std::vector<Node>& lemmas)
 {
   Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end() );
@@ -706,7 +709,7 @@ bool ArithInstantiator::postProcessInstantiationForVariable(
 void DtInstantiator::reset(CegInstantiator* ci,
                            SolvedForm& sf,
                            Node pv,
-                           InstEffort effort)
+                           CegInstEffort effort)
 {
 }
 
@@ -755,10 +758,11 @@ bool DtInstantiator::processEqualTerms(CegInstantiator* ci,
                                        SolvedForm& sf,
                                        Node pv,
                                        std::vector<Node>& eqc,
-                                       InstEffort effort)
+                                       CegInstEffort effort)
 {
-  Trace("cegqi-dt-debug") << "[2] try based on constructors in equivalence class." << std::endl;
-  //[2] look in equivalence class for a constructor
+  Trace("cegqi-dt-debug") << "try based on constructors in equivalence class."
+                          << std::endl;
+  // look in equivalence class for a constructor
   for( unsigned k=0; k<eqc.size(); k++ ){
     Node n = eqc[k];
     if( n.getKind()==APPLY_CONSTRUCTOR ){
@@ -795,7 +799,7 @@ bool DtInstantiator::processEquality(CegInstantiator* ci,
                                      Node pv,
                                      std::vector<TermProperties>& term_props,
                                      std::vector<Node>& terms,
-                                     InstEffort effort)
+                                     CegInstEffort effort)
 {
   Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] );
   if( !val.isNull() ){
@@ -811,7 +815,7 @@ bool DtInstantiator::processEquality(CegInstantiator* ci,
 void EprInstantiator::reset(CegInstantiator* ci,
                             SolvedForm& sf,
                             Node pv,
-                            InstEffort effort)
+                            CegInstEffort effort)
 {
   d_equal_terms.clear();
 }
@@ -821,7 +825,7 @@ bool EprInstantiator::processEqualTerm(CegInstantiator* ci,
                                        Node pv,
                                        TermProperties& pv_prop,
                                        Node n,
-                                       InstEffort effort)
+                                       CegInstEffort effort)
 {
   if( options::quantEprMatching() ){
     Assert( pv_prop.isBasic() );
@@ -887,7 +891,7 @@ bool EprInstantiator::processEqualTerms(CegInstantiator* ci,
                                         SolvedForm& sf,
                                         Node pv,
                                         std::vector<Node>& eqc,
-                                        InstEffort effort)
+                                        CegInstEffort effort)
 {
   if( options::quantEprMatching() ){
     //heuristic for best matching constant
@@ -945,7 +949,7 @@ BvInstantiator::~BvInstantiator(){
 void BvInstantiator::reset(CegInstantiator* ci,
                            SolvedForm& sf,
                            Node pv,
-                           InstEffort effort)
+                           CegInstEffort effort)
 {
   d_inst_id_counter = 0;
   d_var_to_inst_id.clear();
@@ -961,7 +965,7 @@ void BvInstantiator::processLiteral(CegInstantiator* ci,
                                     Node pv,
                                     Node lit,
                                     Node alit,
-                                    InstEffort effort)
+                                    CegInstEffort effort)
 {
   Assert( d_inverter!=NULL );
   // find path to pv
@@ -991,8 +995,11 @@ void BvInstantiator::processLiteral(CegInstantiator* ci,
   }
 }
 
-Node BvInstantiator::hasProcessAssertion(
-    CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, InstEffort effort)
+Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
+                                         SolvedForm& sf,
+                                         Node pv,
+                                         Node lit,
+                                         CegInstEffort effort)
 {
   Node atom = lit.getKind() == NOT ? lit[0] : lit;
   bool pol = lit.getKind() != NOT;
@@ -1088,7 +1095,7 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci,
                                       Node pv,
                                       Node lit,
                                       Node alit,
-                                      InstEffort effort)
+                                      CegInstEffort effort)
 {
   // if option enabled, use approach for word-level inversion for BV instantiation
   if( options::cbqiBv() ){
@@ -1109,7 +1116,7 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci,
 bool BvInstantiator::processAssertions(CegInstantiator* ci,
                                        SolvedForm& sf,
                                        Node pv,
-                                       InstEffort effort)
+                                       CegInstEffort effort)
 {
   std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction >::iterator iti = d_var_to_inst_id.find( pv );
   if( iti!=d_var_to_inst_id.end() ){
@@ -1162,18 +1169,6 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci,
             Trace("cegqi-bv") << "   ...with slack value : " << curr_slack_val
                               << std::endl;
           }
-          // process information about solved status
-          std::unordered_map<unsigned, BvInverterStatus>::iterator its =
-              d_inst_id_to_status.find(inst_id);
-          Assert(its != d_inst_id_to_status.end());
-          if (!its->second.d_conds.empty()) {
-            Trace("cegqi-bv") << "   ...with " << its->second.d_conds.size()
-                              << " side conditions : " << std::endl;
-            for (unsigned k = 0; k < its->second.d_conds.size(); k++) {
-              Node cond = its->second.d_conds[k];
-              Trace("cegqi-bv") << "       " << cond << std::endl;
-            }
-          }
           Trace("cegqi-bv") << std::endl;
         }
 
@@ -1325,6 +1320,14 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci,
 
       visited.top()[cur] = ret;
     }
+    else if (Trace.isOn("cegqi-bv-nl"))
+    {
+      if (cur == pv)
+      {
+        Trace("cegqi-bv-nl") << "NONLINEAR LITERAL for " << pv << " : " << lit
+                             << std::endl;
+      }
+    }
   } while (!visit.top().empty());
   Assert(visited.size() == 1);
   Assert(visited.top().find(lit) != visited.top().end());
@@ -1362,6 +1365,165 @@ Node BvInstantiator::rewriteTermForSolvePv(
   return Node::null();
 }
 
+/** sort bv extract interval
+ *
+ * This sorts lists of bitvector extract terms where
+ * ((_ extract i1 i2) t) < ((_ extract j1 j2) t)
+ * if i1>j1 or i1=j1 and i2>j2.
+ */
+struct SortBvExtractInterval
+{
+  bool operator()(Node i, Node j)
+  {
+    Assert(i.getKind() == BITVECTOR_EXTRACT);
+    Assert(j.getKind() == BITVECTOR_EXTRACT);
+    BitVectorExtract ie = i.getOperator().getConst<BitVectorExtract>();
+    BitVectorExtract je = j.getOperator().getConst<BitVectorExtract>();
+    if (ie.high > je.high)
+    {
+      return true;
+    }
+    else if (ie.high == je.high)
+    {
+      Assert(ie.low != je.low);
+      return ie.low > je.low;
+    }
+    return false;
+  }
+};
+
+void BvInstantiatorPreprocess::registerCounterexampleLemma(
+    std::vector<Node>& lems, std::vector<Node>& ce_vars)
+{
+  // new variables
+  std::vector<Node> vars;
+  // new lemmas
+  std::vector<Node> new_lems;
+
+  if (options::cbqiBvRmExtract())
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl;
+    // map from terms to bitvector extracts applied to that term
+    std::map<Node, std::vector<Node> > extract_map;
+    std::unordered_set<TNode, TNodeHashFunction> visited;
+    for (unsigned i = 0, size = lems.size(); i < size; i++)
+    {
+      Trace("cegqi-bv-pp-debug2") << "Register ce lemma # " << i << " : "
+                                  << lems[i] << std::endl;
+      collectExtracts(lems[i], extract_map, visited);
+    }
+    for (std::pair<const Node, std::vector<Node> >& es : extract_map)
+    {
+      if (es.second.size() > 1)
+      {
+        // sort based on the extract start position
+        std::vector<Node>& curr_vec = es.second;
+
+        SortBvExtractInterval sbei;
+        std::sort(curr_vec.begin(), curr_vec.end(), sbei);
+
+        unsigned width = es.first.getType().getBitVectorSize();
+
+        // list of points b such that:
+        //   b>0 and we must start a segment at (b-1)  or  b==0
+        std::vector<unsigned> boundaries;
+        boundaries.push_back(width);
+        boundaries.push_back(0);
+
+        Trace("cegqi-bv-pp") << "For term " << es.first << " : " << std::endl;
+        for (unsigned i = 0, size = curr_vec.size(); i < size; i++)
+        {
+          Trace("cegqi-bv-pp") << "  " << i << " : " << curr_vec[i]
+                               << std::endl;
+          BitVectorExtract e =
+              curr_vec[i].getOperator().getConst<BitVectorExtract>();
+          if (std::find(boundaries.begin(), boundaries.end(), e.high + 1)
+              == boundaries.end())
+          {
+            boundaries.push_back(e.high + 1);
+          }
+          if (std::find(boundaries.begin(), boundaries.end(), e.low)
+              == boundaries.end())
+          {
+            boundaries.push_back(e.low);
+          }
+        }
+        std::sort(boundaries.rbegin(), boundaries.rend());
+
+        // make the extract variables
+        std::vector<Node> children;
+        for (unsigned i = 1; i < boundaries.size(); i++)
+        {
+          Assert(boundaries[i - 1] > 0);
+          Node ex = bv::utils::mkExtract(
+              es.first, boundaries[i - 1] - 1, boundaries[i]);
+          Node var =
+              nm->mkSkolem("ek",
+                           ex.getType(),
+                           "variable to represent disjoint extract region");
+          Node ceq_lem = var.eqNode(ex);
+          Trace("cegqi-bv-pp") << "Introduced : " << ceq_lem << std::endl;
+          new_lems.push_back(ceq_lem);
+          children.push_back(var);
+          vars.push_back(var);
+        }
+
+        Node conc = nm->mkNode(kind::BITVECTOR_CONCAT, children);
+        Assert(conc.getType() == es.first.getType());
+        Node eq_lem = conc.eqNode(es.first);
+        Trace("cegqi-bv-pp") << "Introduced : " << eq_lem << std::endl;
+        new_lems.push_back(eq_lem);
+      }
+      Trace("cegqi-bv-pp") << "...finished processing extracts for term "
+                            << es.first << std::endl;
+    }
+    Trace("cegqi-bv-pp") << "-----done remove extracts" << std::endl;
+  }
+
+  if (!vars.empty())
+  {
+    // could try applying subs -> vars here
+    // in practice, this led to worse performance
+
+    Trace("cegqi-bv-pp") << "Adding " << new_lems.size() << " lemmas..."
+                         << std::endl;
+    lems.insert(lems.end(), new_lems.begin(), new_lems.end());
+    Trace("cegqi-bv-pp") << "Adding " << vars.size() << " variables..."
+                         << std::endl;
+    ce_vars.insert(ce_vars.end(), vars.begin(), vars.end());
+  }
+}
+
+void BvInstantiatorPreprocess::collectExtracts(
+    Node lem,
+    std::map<Node, std::vector<Node> >& extract_map,
+    std::unordered_set<TNode, TNodeHashFunction>& visited)
+{
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(lem);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+
+      if (cur.getKind() == BITVECTOR_EXTRACT)
+      {
+        extract_map[cur[0]].push_back(cur);
+      }
+
+      for (const Node& nc : cur)
+      {
+        visit.push_back(nc);
+      }
+    }
+  } while (!visit.empty());
+}
+
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index 0242a2994..4fb954d44 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -36,11 +36,11 @@ class ArithInstantiator : public Instantiator {
   virtual void reset(CegInstantiator* ci,
                      SolvedForm& sf,
                      Node pv,
-                     InstEffort effort) override;
+                     CegInstEffort effort) override;
   virtual bool hasProcessEquality(CegInstantiator* ci,
                                   SolvedForm& sf,
                                   Node pv,
-                                  InstEffort effort) override
+                                  CegInstEffort effort) override
   {
     return true;
   }
@@ -49,11 +49,11 @@ class ArithInstantiator : public Instantiator {
                                Node pv,
                                std::vector<TermProperties>& term_props,
                                std::vector<Node>& terms,
-                               InstEffort effort) override;
+                               CegInstEffort effort) override;
   virtual bool hasProcessAssertion(CegInstantiator* ci,
                                    SolvedForm& sf,
                                    Node pv,
-                                   InstEffort effort) override
+                                   CegInstEffort effort) override
   {
     return true;
   }
@@ -61,24 +61,27 @@ class ArithInstantiator : public Instantiator {
                                    SolvedForm& sf,
                                    Node pv,
                                    Node lit,
-                                   InstEffort effort) override;
+                                   CegInstEffort effort) override;
   virtual bool processAssertion(CegInstantiator* ci,
                                 SolvedForm& sf,
                                 Node pv,
                                 Node lit,
                                 Node alit,
-                                InstEffort effort) override;
+                                CegInstEffort effort) override;
   virtual bool processAssertions(CegInstantiator* ci,
                                  SolvedForm& sf,
                                  Node pv,
-                                 InstEffort effort) override;
+                                 CegInstEffort effort) override;
   virtual bool needsPostProcessInstantiationForVariable(
-      CegInstantiator* ci, SolvedForm& sf, Node pv, InstEffort effort) override;
+      CegInstantiator* ci,
+      SolvedForm& sf,
+      Node pv,
+      CegInstEffort effort) override;
   virtual bool postProcessInstantiationForVariable(
       CegInstantiator* ci,
       SolvedForm& sf,
       Node pv,
-      InstEffort effort,
+      CegInstEffort effort,
       std::vector<Node>& lemmas) override;
   virtual std::string identify() const override { return "Arith"; }
  private:
@@ -113,16 +116,16 @@ public:
   virtual void reset(CegInstantiator* ci,
                      SolvedForm& sf,
                      Node pv,
-                     InstEffort effort) override;
+                     CegInstEffort effort) override;
   virtual bool processEqualTerms(CegInstantiator* ci,
                                  SolvedForm& sf,
                                  Node pv,
                                  std::vector<Node>& eqc,
-                                 InstEffort effort) override;
+                                 CegInstEffort effort) override;
   virtual bool hasProcessEquality(CegInstantiator* ci,
                                   SolvedForm& sf,
                                   Node pv,
-                                  InstEffort effort) override
+                                  CegInstEffort effort) override
   {
     return true;
   }
@@ -131,7 +134,7 @@ public:
                                Node pv,
                                std::vector<TermProperties>& term_props,
                                std::vector<Node>& terms,
-                               InstEffort effort) override;
+                               CegInstEffort effort) override;
   virtual std::string identify() const override { return "Dt"; }
  private:
   Node solve_dt(Node v, Node a, Node b, Node sa, Node sb);
@@ -146,18 +149,18 @@ class EprInstantiator : public Instantiator {
   virtual void reset(CegInstantiator* ci,
                      SolvedForm& sf,
                      Node pv,
-                     InstEffort effort) override;
+                     CegInstEffort effort) override;
   virtual bool processEqualTerm(CegInstantiator* ci,
                                 SolvedForm& sf,
                                 Node pv,
                                 TermProperties& pv_prop,
                                 Node n,
-                                InstEffort effort) override;
+                                CegInstEffort effort) override;
   virtual bool processEqualTerms(CegInstantiator* ci,
                                  SolvedForm& sf,
                                  Node pv,
                                  std::vector<Node>& eqc,
-                                 InstEffort effort) override;
+                                 CegInstEffort effort) override;
   virtual std::string identify() const override { return "Epr"; }
  private:
   std::vector<Node> d_equal_terms;
@@ -188,11 +191,11 @@ class BvInstantiator : public Instantiator {
   virtual void reset(CegInstantiator* ci,
                      SolvedForm& sf,
                      Node pv,
-                     InstEffort effort) override;
+                     CegInstEffort effort) override;
   virtual bool hasProcessAssertion(CegInstantiator* ci,
                                    SolvedForm& sf,
                                    Node pv,
-                                   InstEffort effort) override
+                                   CegInstEffort effort) override
   {
     return true;
   }
@@ -200,21 +203,21 @@ class BvInstantiator : public Instantiator {
                                    SolvedForm& sf,
                                    Node pv,
                                    Node lit,
-                                   InstEffort effort) override;
+                                   CegInstEffort effort) override;
   virtual bool processAssertion(CegInstantiator* ci,
                                 SolvedForm& sf,
                                 Node pv,
                                 Node lit,
                                 Node alit,
-                                InstEffort effort) override;
+                                CegInstEffort effort) override;
   virtual bool processAssertions(CegInstantiator* ci,
                                  SolvedForm& sf,
                                  Node pv,
-                                 InstEffort effort) override;
+                                 CegInstEffort effort) override;
   virtual bool useModelValue(CegInstantiator* ci,
                              SolvedForm& sf,
                              Node pv,
-                             InstEffort effort) override
+                             CegInstEffort effort) override
   {
     return true;
   }
@@ -262,7 +265,61 @@ class BvInstantiator : public Instantiator {
                       Node pv,
                       Node lit,
                       Node alit,
-                      InstEffort effort);
+                      CegInstEffort effort);
+};
+
+/** Bitvector instantiator preprocess
+ *
+ * This class implements preprocess techniques that are helpful for
+ * counterexample-guided instantiation, such as introducing variables
+ * that refer to disjoint bit-vector extracts.
+ */
+class BvInstantiatorPreprocess : public InstantiatorPreprocess
+{
+ public:
+  BvInstantiatorPreprocess() {}
+  virtual ~BvInstantiatorPreprocess() {}
+  /** register counterexample lemma
+   *
+   * This method modifies the contents of lems based on removing extract terms
+   * when the option --cbqi-bv-rm-extract is enabled.
+   *
+   * For example:
+   *   P[ ((extract 7 4) t), ((extract 3 0) t)]
+   *     becomes:
+   *   P[((extract 7 4) t), ((extract 3 0) t)] ^
+   *   t = concat( x74, x30 ) ^
+   *   x74 = ((extract 7 4) t) ^
+   *   x30 = ((extract 3 0) t)
+   * where x74 and x30 are fresh variables.
+   *
+   * Another example:
+   *   P[ ((extract 7 3) t), ((extract 4 0) t)]
+   *     becomes:
+   *   P[((extract 7 4) t), ((extract 3 0) t)] ^
+   *   t = concat( x75, x44, x30 ) ^
+   *   x75 = ((extract 7 5) t) ^
+   *   x44 = ((extract 4 4) t) ^
+   *   x30 = ((extract 3 0) t)
+   * where x75, x44 and x30 are fresh variables.
+   *
+   * Notice we leave the original conjecture alone. This is done for performance
+   * since the added equalities ensure we are able to construct the proper
+   * solved forms for variables in t and for the intermediate variables above.
+   */
+  virtual void registerCounterexampleLemma(std::vector<Node>& lems,
+                                           std::vector<Node>& ce_vars) override;
+
+ private:
+  /** collect extracts
+   *
+   * This method collects all extract terms in lem
+   * and stores them in d_extract_map.
+   * visited is the terms we've already visited.
+   */
+  void collectExtracts(Node lem,
+                       std::map<Node, std::vector<Node> >& extract_map,
+                       std::unordered_set<TNode, TNodeHashFunction>& visited);
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 274dcaff0..c59570651 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -115,6 +115,7 @@ TESTS =	\
 	NUM878.smt2 \
 	psyco-107-bv.smt2 \
 	ari118-bv-2occ-x.smt2 \
+	extract-nproc.smt2 \
 	javafe.ast.StandardPrettyPrint.319.smt2 \
 	javafe.ast.StmtVec.009.smt2 \
 	javafe.ast.WhileStmt.447.smt2 \
diff --git a/test/regress/regress0/sygus/Base16_1.sy b/test/regress/regress0/sygus/Base16_1.sy
new file mode 100644
index 000000000..5833751cb
--- /dev/null
+++ b/test/regress/regress0/sygus/Base16_1.sy
@@ -0,0 +1,34 @@
+; EXPECT: unsat
+; COMMAND-LINE:  --sygus-qe-preproc --cbqi-bv-rm-extract --sygus-out=status --cbqi-bv --cegqi-si=all
+(set-logic BV)
+
+(define-fun B ((h (BitVec 8)) (l (BitVec 8)) (v (BitVec 8))) (BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l))))
+
+(define-fun E ((x (BitVec 8))) (BitVec 8)  (bvadd x #x41))
+
+(define-fun f ((x (BitVec 8))) (BitVec 8) (bvsub x #x41))
+
+(define-fun d ((x (BitVec 8))) Bool (bvule x #x3f))
+
+(synth-fun D ((x (BitVec 8)) (y (BitVec 8)) ) (BitVec 8)
+    	((Start (BitVec 8) (
+			(f Start) x y Const
+				(bvshl Start Start) 	 (bvnot Start)
+						 (bvand Start Start)
+						 (bvxor Start Start)
+						 (bvor Start Start)
+						 (bvneg Start)
+						 (bvadd Start Start)
+						 (bvlshr Start Start)
+						 (bvsub Start Start)
+			))
+	 (Const (BitVec 8) (#x01 #x03 #x06 #x07 #x04 #x05 #x02 #x00))
+))
+
+(declare-var x (BitVec 8))
+(constraint  (= x (D (E (B #x07 #x04 x) ) (E  (B #x03 #x00 x))  )) )
+
+; notice we don't have solution reconstruction for this
+(check-synth)    
+
+
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index b40ee845f..82c2c2458 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -70,7 +70,8 @@ TESTS = commutative.sy \
         process-10-vars.sy \
         process-10-vars-2fun.sy \
         inv-unused.sy \
-        ccp16.lus.sy
+        ccp16.lus.sy \
+        Base16_1.sy
 
 
 # sygus tests currently taking too long for make regress