mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix #2813

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-20 15:42:03 -08:00
parent 485ca725de
commit cb21f70cc3
2 changed files with 13 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.h
View file

@ -956,7 +956,7 @@ namespace smt {
public:
void assign(literal l, const b_justification & j, bool decision = false) {
SASSERT(l != false_literal);
// SASSERT(l != false_literal);
SASSERT(l != null_literal);
switch (get_assignment(l)) {
case l_false:

17
src/smt/theory_arith_int.h
View file

@ -667,11 +667,18 @@ namespace smt {
l = ctx.get_literal(bound);
ctx.mark_as_relevant(l);
dump_lemmas(l, ante);
ctx.assign(l, ctx.mk_justification(
gomory_cut_justification(
get_id(), ctx.get_region(),
ante.lits().size(), ante.lits().c_ptr(),
ante.eqs().size(), ante.eqs().c_ptr(), ante, l)));
auto js = ctx.mk_justification(
gomory_cut_justification(
get_id(), ctx.get_region(),
ante.lits().size(), ante.lits().c_ptr(),
ante.eqs().size(), ante.eqs().c_ptr(), ante, l));
if (l == false_literal) {
ctx.mk_clause(0, nullptr, js, CLS_TH_LEMMA, nullptr);
}
else {
ctx.assign(l, js);
}
return true;
}