diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 17:31:35 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 17:31:35 +0000 |
| commit | 43dd3569232fd72d7791db7dd113bdff0bdf916d (patch) | |
| tree | 583e424a623665c7de1195cb6da1bd25e1c91145 /src/theory/ite_simplifier.cpp | |
| parent | 95df801fff9c60b4c69abba0a745011a43779c9f (diff) | |
Fixed bug causing QF_LIA/solver_cvc4/incorrect1.smt and QF_LIA/solver_cvc4/incorrect3.smt
Diffstat (limited to 'src/theory/ite_simplifier.cpp')
| -rw-r--r-- | src/theory/ite_simplifier.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp index c70e9be6a..bf031fc94 100644 --- a/src/theory/ite_simplifier.cpp +++ b/src/theory/ite_simplifier.cpp @@ -369,10 +369,10 @@ Node ITESimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cache) } Node result = builder; - it = substTable.find(result); - if (it != iend) { - result = substitute(it->second, substTable, cache); - } + // it = substTable.find(result); + // if (it != iend) { + // result = substitute(it->second, substTable, cache); + // } cache[e] = result; return result; } |