mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

fix topological traversal crash

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-28 11:59:17 +09:00
parent b79d1a6956
commit 30de514a88
2 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/test/heap.cpp
View file

@ -19,20 +19,19 @@ Revision History:
#include<iostream> #include<iostream>
#include "util/util.h" #include "util/util.h"
#include "util/heap.h" #include "util/heap.h"
#include "util/hashtable.h"
#include "util/trace.h" #include "util/trace.h"
#include "util/uint_set.h"
struct lt_proc { bool operator()(int v1, int v2) const { return v1 < v2; } }; struct lt_proc { bool operator()(int v1, int v2) const { return v1 < v2; } };
typedef heap<lt_proc> int_heap; typedef heap<lt_proc> int_heap;
struct int_hash_proc { unsigned operator()(int v) const { return v * 17; }}; struct int_hash_proc { unsigned operator()(int v) const { return v * 17; }};
typedef int_hashtable<int_hash_proc, default_eq<int> > int_set;
#define N 10000 #define N 10000
static random_gen heap_rand(1); static random_gen heap_rand(1);
static void tst1() { static void tst1() {
int_heap h(N); int_heap h(N);
int_set t; uint_set t;
for (int i = 0; i < N * 3; i++) { for (int i = 0; i < N * 3; i++) {
int val = heap_rand() % N; int val = heap_rand() % N;
if (!h.contains(val)) { if (!h.contains(val)) {
@ -41,14 +40,15 @@ static void tst1() {
t.insert(val); t.insert(val);
} }
else { else {
if (!t.contains(val)) {
for (int v : t) std::cout << v << "\n";
}
ENSURE(t.contains(val)); ENSURE(t.contains(val));
} }
} }
ENSURE(h.check_invariant()); ENSURE(h.check_invariant());
int_set::iterator it = t.begin(); for (int v : t) {
int_set::iterator end = t.end(); ENSURE(h.contains(v));
for (; it != end; ++it) {
ENSURE(h.contains(*it));
} }
while (!h.empty()) { while (!h.empty()) {
int m1 = h.min_value(); int m1 = h.min_value();
@ -84,6 +84,8 @@ static void dump_heap(const int_heap2 & h, std::ostream & out) {
static void tst2() { static void tst2() {
int_heap2 h(N); int_heap2 h(N);
for (int i = 0; i < N * 10; i++) { for (int i = 0; i < N * 10; i++) {
if (i % 1 == 0) std::cout << "i: " << i << std::endl;
if (i % 1000 == 0) std::cout << "i: " << i << std::endl; if (i % 1000 == 0) std::cout << "i: " << i << std::endl;
int cmd = heap_rand() % 10; int cmd = heap_rand() % 10;
if (cmd <= 3) { if (cmd <= 3) {
@ -134,6 +136,7 @@ void tst_heap() {
enable_trace("heap"); enable_trace("heap");
unsigned i = 0; unsigned i = 0;
while (i < 3) { while (i < 3) {
IF_VERBOSE(1, verbose_stream() << "test\n";);
heap_rand.set_seed(i++); heap_rand.set_seed(i++);
tst1(); tst1();
init_values(); init_values();

2
src/util/top_sort.h
View file

@ -42,7 +42,7 @@ class top_sort {
unsigned p_id = 0; unsigned p_id = 0;
if (m_dfs_num.find(f, p_id)) { if (m_dfs_num.find(f, p_id)) {
if (!m_partition_id.contains(f)) { if (!m_partition_id.contains(f)) {
while (!m_stack_P.empty() && m_partition_id[m_stack_P.back()] > p_id) { while (!m_stack_P.empty() && m_partition_id.contains(m_stack_P.back()) && m_partition_id[m_stack_P.back()] > p_id) {
m_stack_P.pop_back(); m_stack_P.pop_back();
} }
} }