mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-10 01:42:04 -08:00
parent d0b47d23f6
commit c1d58088be
3 changed files with 10 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -226,7 +226,7 @@ namespace polysat {
}
clause_builder conflict::build_lemma() {
SASSERT(std::all_of(m_vars.begin(), m_vars.end(), [&](pvar v) { return s.is_assigned(v); }));
// SASSERT(std::all_of(m_vars.begin(), m_vars.end(), [&](pvar v) { return s.is_assigned(v); }));
SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c) { return !c->has_bvar(); }));
LOG_H3("Build lemma from core");

11
src/test/polysat.cpp
View file

@ -1076,9 +1076,6 @@ void tst_polysat() {
polysat::test_ineq_axiom5();
polysat::test_ineq_axiom6();
// not working
// polysat::test_fixed_point_arith_div_mul_inverse();
// polysat::test_monot_bounds_simple(8);
// working
// NOT: polysat::test_fixed_point_arith_mul_div_inverse();
@ -1127,6 +1124,14 @@ void tst_polysat() {
polysat::test_ineq1();
polysat::test_ineq2();
#endif
// not working
polysat::test_monot_bounds_simple(8);
polysat::test_fixed_point_arith_div_mul_inverse();
polysat::test_monot();
polysat::test_ineq2();
polysat::test_ineq1();
}

2
src/util/uint_set.h
View file

@ -192,7 +192,7 @@ public:
m_set(&s), m_index(at_end?s.get_max_elem():0), m_last(s.get_max_elem()) {
scan();
SASSERT(invariant());
}
}
unsigned operator*() const { return m_index; }
bool operator==(iterator const& it) const { return m_index == it.m_index; }
bool operator!=(iterator const& it) const { return m_index != it.m_index; }