Issue with check_sat_cc

[hgvk94]

Instance commit Running z3 with default options causes it to either seg fault:

    frame #0: 0x00000000016eec8b z3`smt::conflict_resolution::process_justifications(this=0x0000000002512f48) at smt_conflict_resolution.cpp:204:21
   201              while (m_todo_js_qhead < sz) {
   202                  justification * js = m_todo_js[m_todo_js_qhead];
   203                  m_todo_js_qhead++;
-> 204                  js->get_antecedents(*this);
   205              }
   206              while (!m_todo_eqs.empty()) {
   207                  enode_pair p = m_todo_eqs.back();
(lldb) bt
* thread #1, name = 'z3', stop reason = signal SIGSEGV: invalid address (fault address: 0xff20)
  * frame #0: 0x00000000016eec8b z3`smt::conflict_resolution::process_justifications(this=0x0000000002512f48) at smt_conflict_resolution.cpp:204:21
    frame #1: 0x00000000016eec02 z3`smt::conflict_resolution::justification2literals_core(this=0x0000000002512f48, js=0x0000000002721388, result=0x0000000002513090) at smt_conflict_resolution.cpp:195:9
    frame #2: 0x00000000016eef5c z3`smt::conflict_resolution::justification2literals(this=0x0000000002512f48, js=0x0000000002721388, result=0x0000000002513090) at smt_conflict_resolution.cpp:241:9
    frame #3: 0x00000000016ef19a z3`smt::conflict_resolution::get_justification_max_lvl(this=0x0000000002512f48, js=0x0000000002721388) at smt_conflict_resolution.cpp:264:9
    frame #4: 0x00000000016ef4cb z3`smt::conflict_resolution::get_max_lvl(this=0x0000000002512f48, consequent=(m_val = 1), js=(m_data = 0x0000000002707058)) at smt_conflict_resolution.cpp:298:33
    frame #5: 0x00000000016eff97 z3`smt::conflict_resolution::initialize_resolve(this=0x0000000002512f48, conflict=(m_data = 0x0000000002707058), not_l=(m_val = -2), js=0x00007fffffff75d8, consequent=0x00007fffffff75d0) at smt_conflict_resolution.cpp:398:31
    frame #6: 0x00000000016f2c1c z3`smt::conflict_resolution::resolve(this=0x0000000002512f48, conflict=(m_data = 0x0000000002707058), not_l=(m_val = -2)) at smt_conflict_resolution.cpp:486:14
    frame #7: 0x000000000172d840 z3`smt::context::resolve_conflict(this=0x000000000251aaa8) at smt_context.cpp:4079:36
    frame #8: 0x000000000171cddb z3`smt::context::decide_clause(this=0x000000000251aaa8) at smt_context.cpp:3320:13
    frame #9: 0x000000000171be58 z3`smt::context::decide(this=0x000000000251aaa8) at smt_context.cpp:1761:21
    frame #10: 0x000000000172b185 z3`smt::context::bounded_search(this=0x000000000251aaa8) at smt_context.cpp:3909:18
    frame #11: 0x0000000001729997 z3`smt::context::search(this=0x000000000251aaa8) at smt_context.cpp:3745:22
    frame #12: 0x000000000172a566 z3`smt::context::check(this=0x000000000251aaa8, cube=0x000000000252c6d0, clauses=0x00007fffffff8bd0) at smt_context.cpp:3650:17
    frame #13: 0x000000000177cc55 z3`smt::kernel::imp::check(this=0x000000000251aaa8, cube=0x000000000252c6d0, clause=0x00007fffffff8bd0) at smt_kernel.cpp:120:29
    frame #14: 0x000000000177bda8 z3`smt::kernel::check(this=0x000000000252c9f0, cube=0x000000000252c6d0, clauses=0x00007fffffff8bd0) at smt_kernel.cpp:336:23
    frame #15: 0x00000000017f546e z3`(anonymous namespace)::smt_solver::check_sat_cc_core(this=0x000000000252c698, cube=0x000000000252c6d0, clauses=0x00007fffffff8bd0) at smt_solver.cpp:200:30
    frame #16: 0x00000000012e06db z3`solver_na2as::check_sat_cc(this=0x000000000252c698, assumptions=0x00000000025358d0, clauses=0x00007fffffff8bd0) at solver_na2as.cpp:73:12
    frame #17: 0x00000000012e3345 z3`pool_solver::check_sat_cc_core(this=0x0000000002535898, cube=0x00000000025358d0, clauses=0x00007fffffff8bd0) at solver_pool.cpp:191:29
    frame #18: 0x00000000012e06db z3`solver_na2as::check_sat_cc(this=0x0000000002535898, assumptions=0x00000000025e0140, clauses=0x00007fffffff8bd0) at solver_na2as.cpp:73:12
    frame #19: 0x000000000210d440 z3`spacer::iuc_solver::check_sat_cc(this=0x00000000025e0098, cube=0x00007fffffff8c00, clauses=0x00007fffffff8bd0) at spacer_iuc_solver.cpp:137:37
    frame #20: 0x00000000020b0c46 z3`spacer::prop_solver::maxsmt(this=0x00000000024d67a8, hard=0x00007fffffff8c00, soft=0x00007fffffff8e50, clauses=0x00007fffffff8bd0) at spacer_prop_solver.cpp:242:24
    frame #21: 0x00000000020b1176 z3`spacer::prop_solver::internal_check_assumptions(this=0x00000000024d67a8, hard_atoms=0x00007fffffff8c00, soft_atoms=0x00007fffffff8e50, clauses=0x00007fffffff8bd0) at spacer_prop_solver.cpp:308:20
    frame #22: 0x00000000020b1a82 z3`spacer::prop_solver::check_assumptions(this=0x00000000024d67a8, _hard=0x00007fffffff9258, soft=0x00007fffffff8e50, clause=0x0000000002523470, num_bg=2, bg=0x000000000271c6b0, solver_id=1) at spacer_prop_solver.cpp:386:17
    frame #23: 0x000000000206d0fa z3`spacer::pred_transformer::check_inductive(this=0x0000000002523388, level=0, state=0x00007fffffff9258, uses_level=0x00007fffffff9334, weakness=0) at spacer_context.cpp:1553:27
    frame #24: 0x00000000020a82ab z3`spacer::lemma_bool_inductive_generalizer::operator(this=0x00000000026ad018, lemma=0x00007fffffffa7c8)(ref<spacer::lemma>&) at spacer_generalizers.cpp:97:16

or throw an assertion violation at file: src/ast/ast.cpp, line 3170:

frame #1: 0x0000000000abbbe8 z3`ast_manager::mk_unit_resolution(this=0x00000000023dab38, num_proofs=4, proofs=0x00007fffffff6cc0, new_fact=0x00000000023dd208) at ast.cpp:3170:9
    frame #2: 0x00000000016f8750 z3`smt::conflict_resolution::get_proof(this=0x0000000002537578, l=(m_val = 1), js=(m_data = 0x00000000026ef3f8)) at smt_conflict_resolution.cpp:1041:24
    frame #3: 0x00000000016f0f8e z3`smt::conflict_resolution::mk_conflict_proof(this=0x0000000002537578, conflict=(m_data = 0x00000000026ef3f8), not_l=(m_val = -2)) at smt_conflict_resolution.cpp:1327:18
    frame #4: 0x00000000016f03c7 z3`smt::conflict_resolution::initialize_resolve(this=0x0000000002537578, conflict=(m_data = 0x00000000026ef3f8), not_l=(m_val = -2), js=0x00007fffffff75a8, consequent=0x00007fffffff75a0) at smt_conflict_resolution.cpp:417:17
    frame #5: 0x00000000016f2c1c z3`smt::conflict_resolution::resolve(this=0x0000000002537578, conflict=(m_data = 0x00000000026ef3f8), not_l=(m_val = -2)) at smt_conflict_resolution.cpp:486:14
    frame #6: 0x000000000172d840 z3`smt::context::resolve_conflict(this=0x000000000251e6e8) at smt_context.cpp:4079:36
    frame #7: 0x000000000171cddb z3`smt::context::decide_clause(this=0x000000000251e6e8) at smt_context.cpp:3320:13
    frame #8: 0x000000000171be58 z3`smt::context::decide(this=0x000000000251e6e8) at smt_context.cpp:1761:21
    frame #9: 0x000000000172b185 z3`smt::context::bounded_search(this=0x000000000251e6e8) at smt_context.cpp:3909:18
    frame #10: 0x0000000001729997 z3`smt::context::search(this=0x000000000251e6e8) at smt_context.cpp:3745:22
    frame #11: 0x000000000172a566 z3`smt::context::check(this=0x000000000251e6e8, cube=0x000000000251b8a0, clauses=0x00007fffffff8ba0) at smt_context.cpp:3650:17
    frame #12: 0x000000000177cc55 z3`smt::kernel::imp::check(this=0x000000000251e6e8, cube=0x000000000251b8a0, clause=0x00007fffffff8ba0) at smt_kernel.cpp:120:29
    frame #13: 0x000000000177bda8 z3`smt::kernel::check(this=0x000000000251bbc0, cube=0x000000000251b8a0, clauses=0x00007fffffff8ba0) at smt_kernel.cpp:336:23
    frame #14: 0x00000000017f546e z3`(anonymous namespace)::smt_solver::check_sat_cc_core(this=0x000000000251b868, cube=0x000000000251b8a0, clauses=0x00007fffffff8ba0) at smt_solver.cpp:200:30
    frame #15: 0x00000000012e06db z3`solver_na2as::check_sat_cc(this=0x000000000251b868, assumptions=0x000000000251d710, clauses=0x00007fffffff8ba0) at solver_na2as.cpp:73:12
    frame #16: 0x00000000012e3345 z3`pool_solver::check_sat_cc_core(this=0x000000000251d6d8, cube=0x000000000251d710, clauses=0x00007fffffff8ba0) at solver_pool.cpp:191:29
    frame #17: 0x00000000012e06db z3`solver_na2as::check_sat_cc(this=0x000000000251d6d8, assumptions=0x00000000025e2b70, clauses=0x00007fffffff8ba0) at solver_na2as.cpp:73:12
    frame #18: 0x000000000210d440 z3`spacer::iuc_solver::check_sat_cc(this=0x00000000025e2ac8, cube=0x00007fffffff8bd0, clauses=0x00007fffffff8ba0) at spacer_iuc_solver.cpp:137:37
    frame #19: 0x00000000020b0c46 z3`spacer::prop_solver::maxsmt(this=0x00000000025149c8, hard=0x00007fffffff8bd0, soft=0x00007fffffff8e20, clauses=0x00007fffffff8ba0) at spacer_prop_solver.cpp:242:24
    frame #20: 0x00000000020b1176 z3`spacer::prop_solver::internal_check_assumptions(this=0x00000000025149c8, hard_atoms=0x00007fffffff8bd0, soft_atoms=0x00007fffffff8e20, clauses=0x00007fffffff8ba0) at spacer_prop_solver.cpp:308:20
    frame #21: 0x00000000020b1a82 z3`spacer::prop_solver::check_assumptions(this=0x00000000025149c8, _hard=0x00007fffffff9228, soft=0x00007fffffff8e20, clause=0x00000000025259b0, num_bg=2, bg=0x00000000026d8cb0, solver_id=1) at spacer_prop_solver.cpp:386:17
    frame #22: 0x000000000206d0fa z3`spacer::pred_transformer::check_inductive(this=0x00000000025258c8, level=0, state=0x00007fffffff9228, uses_level=0x00007fffffff9304, weakness=0) at spacer_context.cpp:1553:27
    frame #23: 0x00000000020a82ab z3`spacer::lemma_bool_inductive_generalizer::operator(this=0x00000000026b8268, lemma=0x00007fffffffa798)(ref<spacer::lemma>&) at spacer_generalizers.cpp:97:16

The behaviour change is random. Sometimes, the behaviour change happens when changing random seeds, sometimes it happens when enabling certain traces.

I have also observed unsoundness in the query right before the query which produces this issue. However, I cannot reproduce unsoundness at the moment.

[hgvk94]

Update: To reproduce unsoundness issue, run this commit on this instance with the option -tr:spacer.ind_gen. It should throw an assertion violation inside solver_pool.cpp. It will dump many benchmarks. The trace file will contain the name of the dumped benchmarks and models for SAT queries.

The dumped benchmark pool_solver_vsolver#1_5.smt2 is an UNSAT instance. If this benchmark is run from the command line, z3 does not terminate. When this benchmark is run from within Spacer, the check-sat-cc function is called with the assumption (or Inv_ext0_n Inv__tr0 Inv__tr1). This call to check-sat-cc will return SAT with a model that falsifies the assumption clause.