diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-09 12:53:31 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-09 19:53:31 +0000 |
commit | 10e9d697e5ac14f921215b2847bd9bc9c035215e (patch) | |
tree | d5621d35271a7ae39ea1542d9722dfabee4404ad /test/regress/CMakeLists.txt | |
parent | 181a175839e3af50a8cf7f80adf635fe612aeaba (diff) |
Reorder ITE rewrites (#6723)
Fixes #6717. Commit 11c1fba added some
new rewrites for ITE. Due to the new rewrites taking precedence over
existing rewrites, it could happen that some of the previous rewrites
did not apply anymore even though they would have further simplified the
ITE. In the example from the issue, (ite c c true) was rewritten to
(or (not T) T) instead of (ite T true true) and then true. The
commit fixes the issue by moving rewrites resulting in
conjunctions/disjunctions to the end.
Diffstat (limited to 'test/regress/CMakeLists.txt')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4ee8e513e..19c689b87 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -163,6 +163,7 @@ set(regress_0_tests regress0/auflia/fuzz05.smtv1.smt2 regress0/auflia/x2.smtv1.smt2 regress0/bool/issue1978.smt2 + regress0/bool/issue6717-ite-rewrite.smt2 regress0/boolean-prec.cvc regress0/boolean-terms-bug-array.smt2 regress0/boolean-terms-kernel1.smt2 |