diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-24 16:41:49 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-24 16:41:49 +0100 |
commit | c563db2aef51fbc3dd6fb465e520a9d0e4bbfbab (patch) | |
tree | b309a492a717cd41238cc7017d64a98e2347cde2 /src | |
parent | 6478f414ad7d6dcbf597db037e81d97175757605 (diff) |
Ensure static-learning adds rewritten assertions. (#5982)
The static-learning preprocessing sometimes added non-rewritten assertions, despite being used in a part of the preprocessor that assumes all assertions to be rewritten. This may then break other passes further down, in the case of #5729 the non-clausal simplification which explicitly asserts that assertions are rewritten. This PR rewrites the respective assertion properly in the static-learning pass.
Fixes #5729.
Diffstat (limited to 'src')
-rw-r--r-- | src/preprocessing/passes/static_learning.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp index 4ab1a038c..d48857396 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -18,6 +18,7 @@ #include <string> #include "expr/node.h" +#include "theory/rewriter.h" namespace CVC4 { namespace preprocessing { @@ -43,7 +44,8 @@ PreprocessingPassResult StaticLearning::applyInternal( } else { - assertionsToPreprocess->replace(i, learned); + assertionsToPreprocess->replace( + i, theory::Rewriter::rewrite(learned.constructNode())); } } return PreprocessingPassResult::NO_CONFLICT; |