summaryrefslogtreecommitdiff
path: root/src/theory/arith/arith_rewriter.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
-rw-r--r--src/theory/arith/arith_rewriter.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index cecbefdee..09cfabdc8 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -261,7 +261,7 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
}else if(reduction.getKind() == kind::LT){
Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
reduction = currNM->mkNode(kind::NOT, geq);
- }else if( Options::rewriteArithEqualities && reduction.getKind() == kind::EQUAL){
+ }else if( Options::current()->rewriteArithEqualities && reduction.getKind() == kind::EQUAL){
Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
Node leq = currNM->mkNode(kind::LEQ, reduction[0], reduction[1]);
reduction = currNM->mkNode(kind::AND, geq, leq);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback