summaryrefslogtreecommitdiff
path: root/src/theory/strings/strings_fmf.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/strings_fmf.cpp')
-rw-r--r--src/theory/strings/strings_fmf.cpp3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp
index 2951c86a2..a3ae03099 100644
--- a/src/theory/strings/strings_fmf.cpp
+++ b/src/theory/strings/strings_fmf.cpp
@@ -85,8 +85,7 @@ Node StringsFmf::StringSumLengthDecisionStrategy::mkLiteral(unsigned i)
return Node::null();
}
NodeManager* nm = NodeManager::currentNM();
- Node lit = nm->mkNode(
- LEQ, d_inputVarLsum.get(), nm->mkConst(CONST_RATIONAL, Rational(i)));
+ Node lit = nm->mkNode(LEQ, d_inputVarLsum.get(), nm->mkConstInt(Rational(i)));
Trace("strings-fmf") << "StringsFMF::mkLiteral: " << lit << std::endl;
return lit;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback