diff options
Diffstat (limited to 'src/theory/quantifiers/single_inv_partition.cpp')
| -rw-r--r-- | src/theory/quantifiers/single_inv_partition.cpp | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index 73bcad535..2725e1826 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -19,7 +19,6 @@ #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "theory/quantifiers/term_util.h" -#include "theory/rewriter.h" using namespace cvc5; using namespace cvc5::kind; @@ -336,7 +335,6 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, cr = cr.substitute( termsNs.begin(), termsNs.end(), subsNs.begin(), subsNs.end()); } - cr = Rewriter::rewrite(cr); Trace("si-prt") << ".....got si=" << singleInvocation << ", result : " << cr << std::endl; d_conjuncts[2].push_back(cr); @@ -349,7 +347,6 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, Assert(si_terms.size() == si_subs.size()); cr = cr.substitute( si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end()); - cr = Rewriter::rewrite(cr); Trace("si-prt") << ".....si version=" << cr << std::endl; d_conjuncts[0].push_back(cr); } |