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, 2 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp index af72e2a7c..dfffe64cf 100644 --- a/src/theory/quantifiers/quant_bound_inference.cpp +++ b/src/theory/quantifiers/quant_bound_inference.cpp @@ -61,10 +61,9 @@ bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard) if (!c.isLargeFinite()) { NodeManager* nm = NodeManager::currentNM(); - Node card = - nm->mkConst(CONST_RATIONAL, Rational(c.getFiniteCardinality())); + Node card = nm->mkConstInt(Rational(c.getFiniteCardinality())); // check if less than fixed upper bound - Node oth = nm->mkConst(CONST_RATIONAL, Rational(maxCard)); + Node oth = nm->mkConstInt(Rational(maxCard)); Node eq = nm->mkNode(LEQ, card, oth); eq = Rewriter::rewrite(eq); mc = eq.isConst() && eq.getConst<bool>(); |