mirror of
https://github.com/Z3Prover/z3
synced 2026-05-09 20:02:23 +00:00
assert backbone to local context in backbone worker
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
725772dfec
commit
abd378e9d8
1 changed files with 1 additions and 0 deletions
|
|
@ -182,6 +182,7 @@ namespace smt {
|
|||
expr_ref not_e(mk_not(m, e), m);
|
||||
if (b.collect_global_backbone(m_l2g, not_e))
|
||||
m_stats.m_backbones_found++;
|
||||
ctx->assert_expr(not_e);
|
||||
units.insert(v);
|
||||
r = l_undef;
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue