mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-01 08:53:18 +00:00
Code Activity

[spacer] fixedpoint.get_answer() returns ground refutation for SAT

Browse source
This commit is contained in:
Arie Gurfinkel 2020-03-31 10:13:37 -04:00
parent 79eb6a0e66
commit cfe96fe92e
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/muz/spacer/spacer_context.h
View file

@ -1016,7 +1016,10 @@ class context {
/** /**
\brief Retrieve satisfying assignment with explanation. \brief Retrieve satisfying assignment with explanation.
*/ */
expr_ref mk_sat_answer() const {return get_ground_sat_answer();} expr_ref mk_sat_answer() const {
proof_ref pr = get_ground_refutation();
return expr_ref(pr.get(), pr.get_manager());
}
expr_ref mk_unsat_answer() const; expr_ref mk_unsat_answer() const;
unsigned get_cex_depth (); unsigned get_cex_depth ();