diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-21 22:51:30 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-21 22:51:30 +0000 |
commit | 22f47a144520f39801abb3acacbf3639886b0478 (patch) | |
tree | 13a5808dac1f0a946e1a14c414a45f16b2a6b00e /test/unit | |
parent | 91829206b4783a532453eab3c69de83b8b510286 (diff) |
* Option --no-type-checking now disables type checks in SmtEngine
* Adding options --lazy-type-checking and --eager-type-checking
to control type checking in NodeBuilder, which can now be enabled
in production mode and disabled in debug mode
* Option --no-checking implies --no-type-checking
* Adding constructor SmtEngine(ExprManager* em) that uses default options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/theory/shared_term_manager_black.h | 2 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h index 3e7a9f523..5007f43ed 100644 --- a/test/unit/theory/shared_term_manager_black.h +++ b/test/unit/theory/shared_term_manager_black.h @@ -61,7 +61,7 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - d_theoryEngine = new TheoryEngine(d_ctxt, &d_options); + d_theoryEngine = new TheoryEngine(d_ctxt, d_options); } void tearDown() { diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 12c38d0d7..00766ec90 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -248,7 +248,7 @@ public: d_bv = new FakeTheory(d_ctxt, *d_nullChannel, "BV"); // create the TheoryEngine - d_theoryEngine = new TheoryEngine(d_ctxt, &d_options); + d_theoryEngine = new TheoryEngine(d_ctxt, d_options); // insert our fake versions into the TheoryEngine's theoryOf table d_theoryEngine->d_theoryOfTable. |