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.

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;