Merge quantifiers2-trunk:

   - new syntax for rewrite rules
   - better rewrite rules theory
   - remove the rewriting with rewrite rules during ppRewrite temporarily
   - theory can define their own candidate generator
   - define a general candidate generator (inefficient ask to every theory)
   - split inst_match between the pattern matching used for quantifiers (inst_match.*) and
     the one used for rewrite rules (rr_inst_match.*):
      - the pattern matching is less exhaustive for quantifiers,
      - the one for rewrite rules can use efficient-e-matching.

1 files changed, 1 insertions, 1 deletions

diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp
index c4cb2f493..ab3a1548e 100644
--- a/src/theory/arith/theory_arith_instantiator.cpp
+++ b/src/theory/arith/theory_arith_instantiator.cpp
@@ -376,7 +376,7 @@ bool InstantiatorTheoryArith::doInstantiation2( Node f, Node term, ArithVar x, I
   }
   instVal = Rewriter::rewrite( instVal );
   //use as instantiation value for var
-  m.d_map[ var ] = instVal;
+  m.set(var, instVal);
   Debug("quant-arith") << "Add instantiation " << m << std::endl;
   return d_quantEngine->addInstantiation( f, m );
 }