From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 24 Feb 2021 15:41:49 +0000 (+0100)
Subject: Ensure static-learning adds rewritten assertions. (#5982)
X-Git-Tag: cvc5-1.0.0~2220
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c563db2aef51fbc3dd6fb465e520a9d0e4bbfbab;p=cvc5.git

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 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;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e4a1251b5..e282deba4 100644
--- 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
index 000000000..56d8bc107
--- /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