mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 08:51:55 +00:00
Code Activity

add sketch of inprocessing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-10 20:13:36 -07:00
parent 6e9e85b213
commit e653f167df
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_parallel2.cpp
View file

@ -342,7 +342,7 @@ namespace smt {
if (!m_config.m_inprocessing) if (!m_config.m_inprocessing)
return; return;
m_config.m_inprocessing = false; // initial strategy is to immediately disable inprocessing for future calls. m_config.m_inprocessing = false; // initial strategy is to immediately disable inprocessing for future calls.
dep_expr_state fmls(m); dep_expr_state fmls(m); // TBD, OH, this also has to be heap allocated for m_simplifier to be valid!
if (!ctx->m_simplifier) { if (!ctx->m_simplifier) {
// create a simplifier if none exists // create a simplifier if none exists
// initialize it to a default pre-processing simplifier. // initialize it to a default pre-processing simplifier.