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

fix unit test build

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-30 14:49:14 -07:00
parent 893265ce94
commit cb5c2d3a98
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/test/diff_logic.cpp
View file

@ -79,11 +79,11 @@ static void tst2() {
ENSURE(g.get_edge_weight(1, 4, w, d) && w == rational(1)); ENSURE(g.get_edge_weight(1, 4, w, d) && w == rational(1));
ENSURE(!g.get_edge_weight(1, 3, w, d)); ENSURE(!g.get_edge_weight(1, 3, w, d));
ENSURE(g.enable_edge(g.add_edge(2, 4, rational(10), l6))); ENSURE(g.enable_edge(g.add_edge(2, 4, rational(10), l6)));
ENSURE(g.is_feasible()); ENSURE(g.is_feasible_dbg());
g.push(); g.push();
ENSURE(g.enable_edge(g.add_edge(3, 0, rational(2), l4))); ENSURE(g.enable_edge(g.add_edge(3, 0, rational(2), l4)));
ENSURE(!g.enable_edge(g.add_edge(0, 1, rational(-1), l5))); ENSURE(!g.enable_edge(g.add_edge(0, 1, rational(-1), l5)));
ENSURE(!g.is_feasible()); ENSURE(!g.is_feasible_dbg());
TRACE("diff_logic", g.display(tout);); TRACE("diff_logic", g.display(tout););
struct proc { struct proc {
bool_vector found; bool_vector found;
@ -104,7 +104,7 @@ static void tst2() {
ENSURE(p.found[5] == true); ENSURE(p.found[5] == true);
ENSURE(p.found[6] == false); ENSURE(p.found[6] == false);
g.pop(1); g.pop(1);
ENSURE(g.is_feasible()); ENSURE(g.is_feasible_dbg());
TRACE("diff_logic", g.display(tout);); TRACE("diff_logic", g.display(tout););
} }