mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

fix #2643

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-18 09:48:46 -07:00
parent 5eead52cc0
commit 724a42b6f2
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/cmd_context/basic_cmds.cpp
View file

@ -180,7 +180,10 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
if (ctx.ignore_check()) if (ctx.ignore_check())
return; return;
expr_ref pr(ctx.m()); expr_ref pr(ctx.m());
pr = ctx.get_check_sat_result()->get_proof(); auto* chsr = ctx.get_check_sat_result();
if (!chsr)
throw cmd_exception("proof is not available");
pr = chsr->get_proof();
if (!pr && !ctx.produce_proofs()) if (!pr && !ctx.produce_proofs())
throw cmd_exception("proof construction is not enabled, use command (set-option :produce-proofs true)"); throw cmd_exception("proof construction is not enabled, use command (set-option :produce-proofs true)");
if (!pr) if (!pr)