diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-14 17:09:59 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-14 17:09:59 -0600 |
| commit | 528e801343c692b0ce8123f8754e069e6523f5dc (patch) | |
| tree | 517c86381e7a0535c376d244c830365d04e3aa62 /src/smt/smt_engine.cpp | |
| parent | 08289dd911aff28110baf0fd815fd912f8b76fd3 (diff) | |
Remove quantifiers rewrite rules infrastructure (#3754)
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ad4d4e1d5..1d96fc207 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3630,12 +3630,6 @@ void SmtEnginePrivate::addFormula( // n is the result of an unknown preprocessing step, add it to dependency map to null ProofManager::currentPM()->addDependence(n, Node::null()); } - // rewrite rules are by default in the unsat core because - // they need to be applied until saturation - if(options::unsatCores() && - n.getKind() == kind::REWRITE_RULE ){ - ProofManager::currentPM()->addUnsatCore(n.toExpr()); - } ); // Add the normalized formula to the queue |