diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-08 22:51:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-08 22:51:08 +0000 |
commit | e256e63588a867b9ea82e03cfc684c2ea2ca1738 (patch) | |
tree | 97583e7952f18934b2751574032b0a48ff8b866c /test/system | |
parent | ffda058e93ac699b1649a87f15418f645bb13312 (diff) |
* 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.)
Diffstat (limited to 'test/system')
-rw-r--r-- | test/system/cvc3_main.cpp | 8 |
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; |