diff options
Diffstat (limited to 'src/theory/fp/theory_fp.cpp')
| -rw-r--r-- | src/theory/fp/theory_fp.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 037b083f4..0b15486e2 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -589,7 +589,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, nm->mkConst(FloatingPointToFPReal( concrete[0].getType().getConst<FloatingPointSize>())), - nm->mkConst(roundTowardPositive), + nm->mkConst(ROUND_TOWARD_POSITIVE), abstractValue)); Node bg = nm->mkNode( @@ -606,7 +606,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, nm->mkConst(FloatingPointToFPReal( concrete[0].getType().getConst<FloatingPointSize>())), - nm->mkConst(roundTowardNegative), + nm->mkConst(ROUND_TOWARD_NEGATIVE), abstractValue)); Node bl = nm->mkNode( |