Ensure static-learning adds rewritten assertions. (#5982)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 24 Feb 2021 15:41:49 +0000 (16:41 +0100)
committerGitHub <noreply@github.com>
Wed, 24 Feb 2021 15:41:49 +0000 (16:41 +0100)
commitc563db2aef51fbc3dd6fb465e520a9d0e4bbfbab
treeb309a492a717cd41238cc7017d64a98e2347cde2
parent6478f414ad7d6dcbf597db037e81d97175757605
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.
src/preprocessing/passes/static_learning.cpp
test/regress/CMakeLists.txt
test/regress/regress0/preprocess/issue5729-rewritten-assertions.smt2 [new file with mode: 0644]