diff options
Diffstat (limited to 'src/theory/quantifiers/quant_bound_inference.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_bound_inference.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp index 83e48bf9c..af72e2a7c 100644 --- a/src/theory/quantifiers/quant_bound_inference.cpp +++ b/src/theory/quantifiers/quant_bound_inference.cpp @@ -61,9 +61,10 @@ bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard) if (!c.isLargeFinite()) { NodeManager* nm = NodeManager::currentNM(); - Node card = nm->mkConst(Rational(c.getFiniteCardinality())); + Node card = + nm->mkConst(CONST_RATIONAL, Rational(c.getFiniteCardinality())); // check if less than fixed upper bound - Node oth = nm->mkConst(Rational(maxCard)); + Node oth = nm->mkConst(CONST_RATIONAL, Rational(maxCard)); Node eq = nm->mkNode(LEQ, card, oth); eq = Rewriter::rewrite(eq); mc = eq.isConst() && eq.getConst<bool>(); |