diff options
| -rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 5caf565c0..994fe83d2 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -1444,7 +1444,7 @@ bool AletheProofPostprocessCallback::update(Node res, { Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0], res); std::vector<Node> new_children = {vp1, children[0]}; - new_args.push_back(nm->mkConst<Rational>(1)); + new_args.push_back(nm->mkConst<Rational>(CONST_RATIONAL, 1)); return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp) && addAletheStep(AletheRule::RESOLUTION, res, @@ -1467,7 +1467,7 @@ bool AletheProofPostprocessCallback::update(Node res, { Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0], res); std::vector<Node> new_children = {vp1, children[0]}; - new_args.push_back(nm->mkConst<Rational>(1)); + new_args.push_back(nm->mkConst<Rational>(CONST_RATIONAL, 1)); return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp) && addAletheStep(AletheRule::RESOLUTION, res, |