1 files changed, 14 insertions, 8 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 54f2a16fe..06fc8898b 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -599,15 +599,21 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No
   }
 }
 
-bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
+bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
   Assert( f.getKind()==FORALL );
   Assert( vars.size()==terms.size() );
   Node body = getInstantiation( f, vars, terms );
+  //do virtual term substitution
+  if( doVts ){
+    body = Rewriter::rewrite( body );
+    Trace("inst-debug") << "Rewrite vts symbols in " << body << std::endl;
+    Node body_r = d_term_db->rewriteVtsSymbols( body );
+    Trace("inst-debug") << "            ...result: " << body_r << std::endl;
+    body = body_r;
+  }
   Trace("inst-assert") << "(assert " << body << ")" << std::endl;
   //make the lemma
-  NodeBuilder<> nb(kind::OR);
-  nb << f.notNode() << body;
-  Node lem = nb;
+  Node lem = NodeManager::currentNM()->mkNode( kind::OR, f.negate(), body );
   //check for duplication
   if( addLemma( lem ) ){
     d_total_inst_debug[f]++;
@@ -805,13 +811,13 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
   d_phase_req_waiting[lit] = req;
 }
 
-bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){
+bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst, bool doVts ){
   std::vector< Node > terms;
   m.getTerms( this, f, terms );
-  return addInstantiation( f, terms, mkRep, modEq, modInst );
+  return addInstantiation( f, terms, mkRep, modEq, modInst, doVts );
 }
 
-bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) {
+bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) {
   // For resource-limiting (also does a time check).
   getOutputChannel().safePoint(options::quantifierStep());
 
@@ -875,7 +881,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
 
   //add the instantiation
   Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
-  bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms );
+  bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms, doVts );
   //report the result
   if( addedInst ){
     Trace("inst-add-debug") << " -> Success." << std::endl;