* Models' SubstitutionMaps are now attached to the user context

  (rather than SAT context)
* Enable part of CVC3 system test (resolves bug 375)
* Fix infinite recursion in beta reduction code (resolves bug 417)
* Some model-building assertions have been added
* Other minor changes

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 1 insertions, 0 deletions

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index d97781ab7..82d602017 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -514,6 +514,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     Node n;
     for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
       n = typeConstSet.nextTypeEnum(t);
+      Assert(!n.isNull(), "out of values for finite type enumeration while building model");
       constantReps[*i] = n;
       Trace("model-builder") << "  New Const: Setting constant rep of " << (*i) << " to " << n << endl;
     }