mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

compile unit tests

Browse source
This commit is contained in:
Jakob Rath 2023-08-14 14:00:41 +02:00
parent 32d66951a8
commit 1f640b96c9
1 changed files with 6 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/test/polysat.cpp
View file

@ -680,9 +680,8 @@ namespace polysat {
s.add_clause(c2, false);
s.m_viable.intersect(x.var(), c1);
s.m_viable.intersect(x.var(), c2);
svector<lbool> fixed;
vector<ptr_vector<viable::entry>> justifications;
VERIFY(!s.m_viable.collect_bit_information(x.var(), false, fixed, justifications));
viable::fixed_bits_info fbi;
VERIFY(!s.m_viable.collect_bit_information(x.var(), false, fbi));
}
// parity(x) >= 3 and bit_1(x)
@ -695,9 +694,8 @@ namespace polysat {
s.add_clause(c2, false);
s.m_viable.intersect(x.var(), c1);
s.m_viable.intersect(x.var(), c2);
svector<lbool> fixed;
vector<ptr_vector<viable::entry>> justifications;
VERIFY(!s.m_viable.collect_bit_information(x.var(), false, fixed, justifications));
viable::fixed_bits_info fbi;
VERIFY(!s.m_viable.collect_bit_information(x.var(), false, fbi));
}
// parity(x) >= 1 and bit_1(x)
@ -710,9 +708,8 @@ namespace polysat {
s.add_clause(c2, false);
s.m_viable.intersect(x.var(), c1);
s.m_viable.intersect(x.var(), c2);
svector<lbool> fixed;
vector<ptr_vector<viable::entry>> justifications;
VERIFY(!s.m_viable.collect_bit_information(x.var(), false, fixed, justifications));
viable::fixed_bits_info fbi;
VERIFY(!s.m_viable.collect_bit_information(x.var(), false, fbi));
}
// 8 * x + 3 == 0 or 8 * x + 5 == 0 is unsat