diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0acd81248..90d21c60d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -931,13 +931,13 @@ void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertion SubrangeBounds bounds = t.getSubrangeBounds(); Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds << endl; if(bounds.lower.hasBound()) { - Node c = NodeManager::currentNM()->mkConst(bounds.lower.getBound()); + Node c = NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound())); Node lb = NodeManager::currentNM()->mkNode(kind::LEQ, c, n); Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb << endl; assertions.push_back(lb); } if(bounds.upper.hasBound()) { - Node c = NodeManager::currentNM()->mkConst(bounds.upper.getBound()); + Node c = NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound())); Node ub = NodeManager::currentNM()->mkNode(kind::LEQ, n, c); Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub << endl; assertions.push_back(ub); |