mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

use bounded pp for cubes

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-07-28 10:15:16 -07:00
parent f7b2407a11
commit 42b42dd89a
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_parallel.cpp
View file

@ -19,6 +19,7 @@ Author:
#include "util/scoped_ptr_vector.h" #include "util/scoped_ptr_vector.h"
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_translation.h" #include "ast/ast_translation.h"
#include "smt/smt_parallel.h" #include "smt/smt_parallel.h"
#include "smt/smt_lookahead.h" #include "smt/smt_lookahead.h"
@ -148,7 +149,7 @@ namespace smt {
} }
IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i; IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i;
if (num_rounds > 0) verbose_stream() << " :round " << num_rounds; if (num_rounds > 0) verbose_stream() << " :round " << num_rounds;
if (c) verbose_stream() << " :cube: " << mk_pp(c, pm); if (c) verbose_stream() << " :cube: " << mk_bounded_pp(c, pm, 3);
verbose_stream() << ")\n";); verbose_stream() << ")\n";);
lbool r = pctx.check(lasms.size(), lasms.c_ptr()); lbool r = pctx.check(lasms.size(), lasms.c_ptr());