diff options
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 22 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/arith/issue4525.smt2 | 4 |
3 files changed, 9 insertions, 18 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 09b6d742a..638f5250e 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1112,14 +1112,8 @@ void TheoryArithPrivate::checkNonLinearLogic(Node term) } } -struct ArithElimOpAttributeId -{ -}; -typedef expr::Attribute<ArithElimOpAttributeId, Node> ArithElimOpAttribute; - Node TheoryArithPrivate::eliminateOperatorsRec(Node n) { - ArithElimOpAttribute aeoa; Trace("arith-elim") << "Begin elim: " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); std::unordered_map<Node, Node, TNodeHashFunction> visited; @@ -1138,18 +1132,11 @@ Node TheoryArithPrivate::eliminateOperatorsRec(Node n) } else if (it == visited.end()) { - if (cur.hasAttribute(aeoa)) - { - visited[cur] = cur.getAttribute(aeoa); - } - else + visited[cur] = Node::null(); + visit.push_back(cur); + for (const Node& cn : cur) { - visited[cur] = Node::null(); - visit.push_back(cur); - for (const Node& cn : cur) - { - visit.push_back(cn); - } + visit.push_back(cn); } } else if (it->second.isNull()) @@ -1180,7 +1167,6 @@ Node TheoryArithPrivate::eliminateOperatorsRec(Node n) // are defined in terms of other non-standard operators. ret = eliminateOperatorsRec(retElim); } - cur.setAttribute(aeoa, ret); visited[cur] = ret; } } while (!visit.empty()); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fbf249e7f..38c60e0e3 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -37,6 +37,7 @@ set(regress_0_tests regress0/arith/issue3413.smt2 regress0/arith/issue3480.smt2 regress0/arith/issue3683.smt2 + regress0/arith/issue4525.smt2 regress0/arith/ite-lift.smt2 regress0/arith/leq.01.smtv1.smt2 regress0/arith/miplib.cvc diff --git a/test/regress/regress0/arith/issue4525.smt2 b/test/regress/regress0/arith/issue4525.smt2 new file mode 100644 index 000000000..ae7e00990 --- /dev/null +++ b/test/regress/regress0/arith/issue4525.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_NRAT) +(assert (> (cot 0.0) (/ 1 0))) +(set-info :status unsat) +(check-sat) |