diff options
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 4a783a6a4..6cf0d9414 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -936,10 +936,10 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { switch(n.getKind()) { case kind::VARIABLE: { DeltaRational drat = d_partialModel.getAssignment(asArithVar(n)); - // FIXME our infinitesimal is fixed here at 1e-06 + const Rational& delta = d_partialModel.getDelta(); return nodeManager-> mkConst( drat.getNoninfinitesimalPart() + - drat.getInfinitesimalPart() * Rational(1, 1000000) ); + drat.getInfinitesimalPart() * delta ); } case kind::EQUAL: // 2 args |