(unsat-core) Assertion violation at cmd_context/cmd_context_to_goal.cpp:34,cmd_context/cmd_context_to_goal.cpp:43

[wintered]

Files t1 and t2 show two related crashes in Z3 debug built.

[591] % z3debug t1.smt2
unsat
ASSERTION VIOLATION
File: ../src/cmd_context/cmd_context_to_goal.cpp
Line: 34
ctx.assertions().size() == ctx.assertion_names().size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[592] % z3release t1.smt2
unsat
Segmentation fault
[593] % z3san t1.smt2
unsat
ASAN:DEADLYSIGNAL
=================================================================
==13574==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x563399d7eeac bp 0x7ffc68dbeca0 sp 0x7ffc68dbea80 T0)
==13574==The signal is caused by a READ memory access.
==13574==Hint: address points to the zero page.
  #0 0x563399d7eeab in assert_exprs_from(cmd_context const&, goal&) ../src/cmd_context/cmd_context_to_goal.cpp:36
  #1 0x563399d3cc47 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:205
  #2 0x563399cd00d8 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2894
  #3 0x563399cd712c in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3000
  #4 0x563399cd712c in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3129
  #5 0x563399c8e885 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3178
  #6 0x56339734fd36 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:90
  #7 0x56339730854e in main ../src/shell/main.cpp:352
  #8 0x7f4faec3db96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #9 0x56339731c859 in _start (/local/suz-local/software/z3san/build-05212020125809-ed92b84/z3+0x213859)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/cmd_context/cmd_context_to_goal.cpp:36 in assert_exprs_from(cmd_context const&, goal&)
==13574==ABORTING
[594] %
[594] % cat t1.smt2
(set-option :unsat_core true)
(set-option :produce-unsat-cores false)
(assert false)
(set-option :rlimit 10)
(check-sat)
(check-sat-using fix-dl-var)
[595] %
[595] % z3debug t2.smt2
unsat
ASSERTION VIOLATION
File: ../src/cmd_context/cmd_context_to_goal.cpp
Line: 43
ctx.assertion_names().empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[596] % z3release t2.smt2
unsat
unsat
[597] % z3san t2.smt2
unsat
unsat
[598] %
[598] % cat t2.smt2
(set-option :unsat_core false)
(set-option :produce-unsat-cores true)
(assert false)
(set-option :rlimit 10)
(check-sat)
(check-sat-using fix-dl-var)
[599] %

OS: Ubuntu 18.04
Commit: ed92b84

[kfriedberger]

Hi @NikolajBjorner .
We stumbled above your code change related to this issue. The code change happened in this line:

z3/src/params/context_params.cpp

Line 146 in 79f0cea

m_unsat_core |= p.get_bool("unsat_core", m_unsat_core);

This looks like a bug. Why is there an disjunction in this line?
If the param for unsat_core is enabled at any time, it can never be disabled afterwards.
There is no comment on this change and no description except the link to this issue (#4424).

[NikolajBjorner]

it is a kludge code for sure
However, you can't (should not) enable unsat cores after the first assertions.
Use cases where unsat cores are toggled on and off over the text API was never supported before.

[kfriedberger]

Doesn't the same rule, i.e. "enable once, and never disable", also apply for model generation or proof production? The corresponding parameters are set a few lines above the mentioned line, but there is no such disjunction.

Are context_params shared across all solver instances? Isn't it possible to have different solver instances within the same context, and these solver instances have different options for proofs, models, and unsat cores? Is this documented somewhere, except as code?