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.

diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp
index 4ab1a038c23a1ef73ce9d40123878c06ace24677..d48857396c5aa3220289c5c62e60a0b894ccb0f8 100644 (file)
--- 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;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e4a1251b5032fc126aa22050ab5084e7caeb7aa6..e282deba4997b372c478958912686a971e281ad8 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -751,6 +751,7 @@ set(regress_0_tests
   regress0/precedence/xor-assoc.cvc
   regress0/precedence/xor-or.cvc
   regress0/preprocess/circuit-prop.smt2
+  regress0/preprocess/issue5729-rewritten-assertions.smt2
   regress0/preprocess/preprocess_00.cvc
   regress0/preprocess/preprocess_01.cvc
   regress0/preprocess/preprocess_02.cvc

diff --git a/test/regress/regress0/preprocess/issue5729-rewritten-assertions.smt2 b/test/regress/regress0/preprocess/issue5729-rewritten-assertions.smt2
new file mode 100644 (file)
index 0000000..56d8bc1
--- /dev/null
+++ b/test/regress/regress0/preprocess/issue5729-rewritten-assertions.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --no-bv-eq-solver
+; EXPECT: sat
+(set-logic QF_ALL)
+(declare-fun x () (_ BitVec 1))
+(assert (= (_ bv0 1) ((_ int2bv 1) (bv2nat x))))
+(check-sat)
\ No newline at end of file