fix for sets/mar2014/..317minimized..

Observed behavior:
  --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143))
with different set of elements in the model for representative and the node
itself.

Issue:
  The trouble with data structure being mainted to ensure that things
for which lemmas have been generated are not generated again. This
data structure (d_pendingEverInserted) needs to be user context
dependent. The bug was in the sequence of steps from requesting that
a lemma be generated to when it actually was. Sequence was:
addToPending (and also adds to pending ever inserted) ->
isComplete (might remove things from pending if requirment met in other ways) ->
getLemma (actually generated the lemma, if requirement not already met)

Resolution:
  adding terms to d_pendingEverInserted was moved from addToPending()
to getLemma().

1 files changed, 14 insertions, 0 deletions

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 8ec25dffd..6e0a71641 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -56,14 +56,26 @@ void TheoryModel::reset(){
 }
 
 Node TheoryModel::getValue(TNode n) const {
+  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) "
+                          << std::endl;
+
   //apply substitutions
   Node nn = d_substitutions.apply(n);
+  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) post-sub:"
+                          << nn << std::endl;
+
   //get value in model
   nn = getModelValue(nn);
+  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) getmodelvalue: "
+                          << nn << std::endl;
+
   if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) {
     //normalize
     nn = Rewriter::rewrite(nn);
   }
+
+  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ):  returning"
+                          << nn << std::endl;
   return nn;
 }
 
@@ -228,6 +240,8 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){
 
 /** add substitution */
 void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
+  Debug("model-builder") << "TheoryModel::addSubstitution("<< x << ", " << t
+                         << ", invalidateCache = " << invalidateCache << ")\n";
   if( !d_substitutions.hasSubstitution( x ) ){
     d_substitutions.addSubstitution( x, t, invalidateCache );
   } else {