diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-23 14:03:49 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-23 14:03:57 +0200 |
| commit | 2064e455674aab26e3632da31998bda8b3fff5f9 (patch) | |
| tree | 524988e058f1fd4c3e79ed5ea73b3f805c6dd42a /src/theory/quantifiers/rewrite_engine.cpp | |
| parent | 49747c4574eec3cfa192ffb6e6a2451b949e8b3e (diff) | |
Do not throw error when codatatype is not well-founded. Add option for disabling codatatype reasoning. Minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/rewrite_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/rewrite_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 7d9fa3344..05e33c7b2 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -39,7 +39,7 @@ struct PrioritySort { RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) { d_true = NodeManager::currentNM()->mkConst( true ); - d_needsSort = true; + d_needsSort = false; } double RewriteEngine::getPriority( Node f ) { |