mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
0439b795b4
commit
33e7dccd42
|
@ -1292,8 +1292,8 @@ namespace smt {
|
|||
IF_VERBOSE(1, verbose_stream()
|
||||
<< "(smt.pb compile sorting network bound: "
|
||||
<< k << " literals: " << in.size()
|
||||
<< " clauses: " << num_compiled_clauses
|
||||
<< " vars: " << num_compiled_vars << ")\n";);
|
||||
<< " clauses: " << sortnw.m_stats.m_num_compiled_clauses
|
||||
<< " vars: " << sortnw.m_stats.m_num_compiled_vars << ")\n";);
|
||||
|
||||
// auxiliary clauses get removed when popping scopes.
|
||||
// we have to recompile the circuit after back-tracking.
|
||||
|
|
Loading…
Reference in a new issue