Shorter explanations for strings based on tracking which parts of normal forms are dependent upon which equalities. Add anti-skolemization module to quantifiers. Disable rewriting of non-clashing equalities between same constructors.

1 files changed, 3 insertions, 1 deletions

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 0eff9bd5d..2ce86852e 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -631,7 +631,9 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       Trace("model-builder") << "  Processing Term: " << n << endl;
       // Record as rep if this node was specified as a representative
       if (tm->d_reps.find(n) != tm->d_reps.end()){
-        Assert(rep.isNull());
+        //AJR: I believe this assertion is too strict, 
+        // e.g. datatypes may assert representative for two constructor terms that are not in the care graph and are merged during collectModelInfo.
+        //Assert(rep.isNull());
         rep = tm->d_reps[n];
         Assert(!rep.isNull() );
         Trace("model-builder") << "  Rep( " << eqc << " ) = " << rep << std::endl;