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

fix #5020

Browse source 
comparison for strict neighbor relation seemed reversed.
Alas, this could introduce additional regressions
This commit is contained in:
Nikolaj Bjorner 2021-02-12 12:24:27 -08:00
parent c808f74591
commit 998cf4c726
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_special_relations.cpp
View file

@ -739,7 +739,8 @@ namespace smt {
bool theory_special_relations::disconnected(graph const& g, dl_var u, dl_var v) const { bool theory_special_relations::disconnected(graph const& g, dl_var u, dl_var v) const {
s_integer val_u = g.get_assignment(u); s_integer val_u = g.get_assignment(u);
s_integer val_v = g.get_assignment(v); s_integer val_v = g.get_assignment(v);
if (val_u == val_v) return u != v; if (val_u == val_v)
return u != v;
if (val_u < val_v) { if (val_u < val_v) {
std::swap(u, v); std::swap(u, v);
std::swap(val_u, val_v); std::swap(val_u, val_v);
@ -1015,7 +1016,7 @@ namespace smt {
return return
g.is_enabled(edge) && g.is_enabled(edge) &&
g.get_assignment(g.get_source(edge)) + s_integer(1) == g.get_assignment(g.get_target(edge)); g.get_assignment(g.get_source(edge)) - s_integer(1) == g.get_assignment(g.get_target(edge));
} }
bool theory_special_relations::is_strict_neighbour_edge(graph const& g, edge_id e) const { bool theory_special_relations::is_strict_neighbour_edge(graph const& g, edge_id e) const {