mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
disable memory finalization after quant_solve unit test. Related to issue #210
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
62a4737d77
commit
459e456f66
|
@ -238,6 +238,7 @@ static void test_quant_solve1() {
|
||||||
test_quant_solver(m, "(exists ((c Cell)) (= (cell c c) c1))", false);
|
test_quant_solver(m, "(exists ((c Cell)) (= (cell c c) c1))", false);
|
||||||
test_quant_solver(m, "(exists ((c Cell)) (= (cell c (cdr c1)) c1))", false);
|
test_quant_solver(m, "(exists ((c Cell)) (= (cell c (cdr c1)) c1))", false);
|
||||||
|
|
||||||
|
|
||||||
test_quant_solver(m, "(exists ((t Tuple)) (= (tuple a P r1) t))");
|
test_quant_solver(m, "(exists ((t Tuple)) (= (tuple a P r1) t))");
|
||||||
test_quant_solver(m, "(exists ((t Tuple)) (= a (first t)))");
|
test_quant_solver(m, "(exists ((t Tuple)) (= a (first t)))");
|
||||||
test_quant_solver(m, "(exists ((t Tuple)) (= P (second t)))");
|
test_quant_solver(m, "(exists ((t Tuple)) (= P (second t)))");
|
||||||
|
@ -253,11 +254,13 @@ void tst_quant_solve() {
|
||||||
|
|
||||||
test_quant_solve1();
|
test_quant_solve1();
|
||||||
|
|
||||||
|
#if 0
|
||||||
memory::finalize();
|
memory::finalize();
|
||||||
#ifdef _WINDOWS
|
#ifdef _WINDOWS
|
||||||
_CrtDumpMemoryLeaks();
|
_CrtDumpMemoryLeaks();
|
||||||
#endif
|
#endif
|
||||||
exit(0);
|
exit(0);
|
||||||
|
#endif
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue