diff options
Diffstat (limited to 'src/preprocessing/passes/unconstrained_simplifier.cpp')
| -rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index db6cb8b72..ae05d6b87 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -30,13 +30,14 @@ #include "util/bitvector.h" #include "util/rational.h" +using namespace std; +using namespace cvc5::kind; +using namespace cvc5::theory; + namespace cvc5 { namespace preprocessing { namespace passes { -using namespace std; -using namespace cvc5::theory; - UnconstrainedSimplifier::UnconstrainedSimplifier( PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "unconstrained-simplifier"), @@ -514,9 +515,9 @@ void UnconstrainedSimplifier::processUnconstrained() if (current.getType().isInteger()) { // div/mult by 1 should have been simplified - Assert(other != nm->mkConst<Rational>(1)); + Assert(other != nm->mkConst(CONST_RATIONAL, Rational(1))); // div by -1 should have been simplified - if (other != nm->mkConst<Rational>(-1)) + if (other != nm->mkConst(CONST_RATIONAL, Rational(-1))) { break; } @@ -529,7 +530,8 @@ void UnconstrainedSimplifier::processUnconstrained() else { // TODO(#2377): could build ITE here - Node test = other.eqNode(nm->mkConst<Rational>(0)); + Node test = + other.eqNode(nm->mkConst(CONST_RATIONAL, Rational(0))); if (rewrite(test) != nm->mkConst<bool>(false)) { break; |