mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix bug in hilbert_basis reset method. Missing reset of m_iseq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-03-29 17:05:17 -07:00
parent 435c6dd365
commit cd48a5164e
2 changed files with 35 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/muz_qe/hilbert_basis.cpp
View file

@ -731,16 +731,26 @@ bool hilbert_basis::is_invalid_offset(offset_t offs) {
void hilbert_basis::reset() { void hilbert_basis::reset() {
m_ineqs.reset(); m_ineqs.reset();
m_basis.reset(); m_iseq.reset();
m_store.reset(); m_store.reset();
m_basis.reset();
m_free_list.reset(); m_free_list.reset();
m_active.reset(); m_sos.reset();
m_passive->reset();
m_passive2->reset();
m_zero.reset(); m_zero.reset();
m_index->reset(1); m_active.reset();
m_ints.reset(); if (m_passive) {
m_passive->reset();
}
if (m_passive2) {
m_passive2->reset();
}
m_cancel = false; m_cancel = false;
if (m_index) {
m_index->reset(1);
}
m_ints.reset();
m_current_ineq = 0;
} }
void hilbert_basis::collect_statistics(statistics& st) const { void hilbert_basis::collect_statistics(statistics& st) const {

20
src/test/hilbert_basis.cpp
View file

@ -524,6 +524,20 @@ static void tst17() {
} }
static void tst18() {
hilbert_basis hb;
hb.add_eq(vec(0, 1), R(0));
hb.add_eq(vec(1, -1), R(2));
saturate_basis(hb);
}
static void tst19() {
hilbert_basis hb;
hb.add_eq(vec(0, 1, 0), R(0));
hb.add_eq(vec(1, -1, 0), R(2));
saturate_basis(hb);
}
void tst_hilbert_basis() { void tst_hilbert_basis() {
std::cout << "hilbert basis test\n"; std::cout << "hilbert basis test\n";
// tst3(); // tst3();
@ -531,9 +545,13 @@ void tst_hilbert_basis() {
g_use_ordered_support = true; g_use_ordered_support = true;
tst17(); tst18();
return; return;
tst19();
return;
tst17();
if (true) { if (true) {
tst1(); tst1();
tst2(); tst2();