Skip to content

Commit

Permalink
fix Inconsistent Results from consequences Interface Based on Constan…
Browse files Browse the repository at this point in the history
…t Names (see: Z3Prover#6916)
  • Loading branch information
ptr1120 committed Jul 4, 2024
1 parent 9f97f32 commit 7520607
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/smt/smt_consequences.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -243,7 +243,7 @@ namespace smt {
lit.neg();

literal lit = mk_diseq(k, v);
literals.push_back(lit);
literals.push_back(~lit);
mk_clause(literals.size(), literals.data(), nullptr);
TRACE("context", display_literals_verbose(tout, literals.size(), literals.data()););
}
Expand Down

0 comments on commit 7520607

Please sign in to comment.