summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2020-12-08 17:03:49 -0800
committerGitHub <noreply@github.com>2020-12-08 17:03:49 -0800
commitd4b2f061182734c8c8efdea38e7afeaca7122fad (patch)
treeb459d9366e63d13d989b03e5c63c22957ead9d58
parent831bf3412fd4d95656539d7d61fe6d3f7150368c (diff)
ite_utilities: Fix infinite loop in compressTerm. (#5629)
Fixes #4610.
-rw-r--r--src/preprocessing/util/ite_utilities.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index c9bf283ac..7e05af698 100644
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -450,7 +450,7 @@ Node ITECompressor::compressTerm(Node toCompress)
if (cmpCnd.isConst())
{
Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
- Node res = compressTerm(toCompress);
+ Node res = compressTerm(branch);
d_compressed[toCompress] = res;
return res;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback