From e33e66212c1a860c9bf5c48aa6f9926e3c0f2630 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 12 Nov 2022 18:03:38 -0800 Subject: [PATCH] propagate values should not flatten and/or also, elim_uncstr should only be disabled on recursive functions --- src/sat/sat_params.pyg | 2 +- src/tactic/core/propagate_values_tactic.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index c35e97b92..7466a1126 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -47,7 +47,7 @@ def_module_params('sat', ('threads', UINT, 1, 'number of parallel threads to use'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'), ('drat.disable', BOOL, False, 'override anything that enables DRAT'), - ('smt.proof', SYMBOL, '', 'add SMT proof to file'), + ('smt.proof', SYMBOL, '', 'add SMT proof log to file'), ('smt.proof.check', BOOL, False, 'check SMT proof while it is created'), ('smt.proof.check_rup', BOOL, True, 'apply forward RUP proof checking'), ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'), diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 041e4d1c2..6b8395fd8 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -213,6 +213,7 @@ public: m_occs(m, true /* track atoms */), m_params(p) { updt_params_core(p); + m_r.set_flat_and_or(false); } tactic * translate(ast_manager & m) override {