diff options
Diffstat (limited to 'src/theory/strings/infer_proof_cons.cpp')
| -rw-r--r-- | src/theory/strings/infer_proof_cons.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index edfb91c64..81da50062 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -499,7 +499,7 @@ void InferProofCons::convert(InferenceId infer, { // it should be the case that lenConstraint => lenReq lenReq = nm->mkNode(STRING_LENGTH, t0) - .eqNode(nm->mkConst(CONST_RATIONAL, Rational(0))) + .eqNode(nm->mkConstInt(Rational(0))) .notNode(); lenSuccess = convertLengthPf(lenReq, lenConstraint, psb); rule = PfRule::CONCAT_CSPLIT; @@ -530,7 +530,7 @@ void InferProofCons::convert(InferenceId infer, { // it should be the case that lenConstraint => lenReq lenReq = nm->mkNode(STRING_LENGTH, t0) - .eqNode(nm->mkConst(CONST_RATIONAL, Rational(0))) + .eqNode(nm->mkConstInt(Rational(0))) .notNode(); lenSuccess = convertLengthPf(lenReq, lenConstraint, psb); rule = PfRule::CONCAT_CPROP; @@ -837,7 +837,7 @@ void InferProofCons::convert(InferenceId infer, std::vector<Node> childrenAE; childrenAE.push_back(eunf); std::vector<Node> argsAE; - argsAE.push_back(nm->mkConst(CONST_RATIONAL, Rational(0))); + argsAE.push_back(nm->mkConstInt(Rational(0))); Node eunfAE = psb.tryStep(PfRule::AND_ELIM, childrenAE, argsAE); Trace("strings-ipc-prefix") << "--- and elim to " << eunfAE << std::endl; |