mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-24 03:57:51 +00:00
Code Activity

wip

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-10-05 16:06:31 -07:00
parent 0d9d4bb46e
commit a50cecaefa
3 changed files with 31 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/conflict.cpp
View file

@ -125,7 +125,6 @@ namespace polysat {
* should appear, otherwise the lemma would be a tautology
*/
void conflict::insert(signed_constraint c) {
if (c.is_always_true())
return;
if (c->is_marked())
@ -321,7 +320,7 @@ namespace polysat {
bool conflict::try_eliminate(pvar v) {
bool has_v = false;
for (auto c : *this)
has_v |= c->contains_var(v);
has_v |= c->is_var_dependent() && c->contains_var(v);
if (!has_v)
return true;
for (auto* engine : ve_engines)