* 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, 4 insertions, 4 deletions

diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp
index a428f605d..13f5e153c 100644
--- a/test/system/cvc3_main.cpp
+++ b/test/system/cvc3_main.cpp
@@ -2140,10 +2140,10 @@ int main(int argc, char** argv)
     test3();
     cout << "\n}\n\ntest4(): {" << endl;
     test4();
-    //if (regressLevel > 0) {
-    //  cout << "\n}\n\ntest5(): {" << endl;
-    //  test5();
-    //}
+    if (regressLevel > 0) {
+      cout << "\n}\n\ntest5(): {" << endl;
+      test5();
+    }
     //cout << "\n}\n\ntest6(): {" << endl;
     //test6();
     cout << "\n}\n\ntest7(): {" << endl;