diff options
Diffstat (limited to 'src/theory/evaluator.cpp')
| -rw-r--r-- | src/theory/evaluator.cpp | 36 |
1 files changed, 6 insertions, 30 deletions
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 516fb1d05..14ccbe9b7 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -792,41 +792,17 @@ EvalResult Evaluator::evalInternal( break; } case kind::BITVECTOR_UDIV: - case kind::BITVECTOR_UDIV_TOTAL: { - if (currNodeVal.getKind() == kind::BITVECTOR_UDIV_TOTAL - || results[currNode[1]].d_bv.getValue() != 0) - { - BitVector res = results[currNode[0]].d_bv; - res = res.unsignedDivTotal(results[currNode[1]].d_bv); - results[currNode] = EvalResult(res); - } - else - { - results[currNode] = EvalResult(); - evalAsNode[currNode] = - needsReconstruct ? reconstruct(currNode, results, evalAsNode) - : currNodeVal; - } + BitVector res = results[currNode[0]].d_bv; + res = res.unsignedDivTotal(results[currNode[1]].d_bv); + results[currNode] = EvalResult(res); break; } case kind::BITVECTOR_UREM: - case kind::BITVECTOR_UREM_TOTAL: { - if (currNodeVal.getKind() == kind::BITVECTOR_UREM_TOTAL - || results[currNode[1]].d_bv.getValue() != 0) - { - BitVector res = results[currNode[0]].d_bv; - res = res.unsignedRemTotal(results[currNode[1]].d_bv); - results[currNode] = EvalResult(res); - } - else - { - results[currNode] = EvalResult(); - evalAsNode[currNode] = - needsReconstruct ? reconstruct(currNode, results, evalAsNode) - : currNodeVal; - } + BitVector res = results[currNode[0]].d_bv; + res = res.unsignedRemTotal(results[currNode[1]].d_bv); + results[currNode] = EvalResult(res); break; } |