mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

test

Browse source
This commit is contained in:
Jakob Rath 2022-12-16 15:00:50 +01:00
parent 3e6e1e1a8a
commit 75a64975b5
1 changed files with 12 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/test/polysat.cpp
View file

@ -1099,6 +1099,7 @@ namespace polysat {
if (lemmas.size() == cnt)
return;
LOG_H1("FAIL: Expected " << cnt << " learned lemmas; got " << lemmas.size() << "!");
SASSERT(false);
if (!collect_test_records)
VERIFY(false);
}
@ -1115,6 +1116,7 @@ namespace polysat {
}
}
LOG_H1("FAIL: Lemma " << c1 << " not deduced!");
SASSERT(false);
if (!collect_test_records)
VERIFY(false);
}
@ -1881,6 +1883,16 @@ void tst_polysat() {
set_log_enabled(false);
}
#if 0
RUN(test_polysat::test_elim1());
RUN(test_polysat::test_elim2());
RUN(test_polysat::test_elim3());
RUN(test_polysat::test_elim4());
RUN(test_polysat::test_elim5());
RUN(test_polysat::test_elim6());
RUN(test_polysat::test_elim7());
#endif
RUN(test_polysat::test_parity1());
RUN(test_polysat::test_parity1b());
RUN(test_polysat::test_parity2());
@ -1917,14 +1929,6 @@ void tst_polysat() {
RUN(test_polysat::test_var_minimize()); // works but var_minimize isn't used (UNSAT before lemma is created)
RUN(test_polysat::test_elim1());
RUN(test_polysat::test_elim2());
RUN(test_polysat::test_elim3());
RUN(test_polysat::test_elim4());
RUN(test_polysat::test_elim5());
RUN(test_polysat::test_elim6());
RUN(test_polysat::test_elim7());
RUN(test_polysat::test_ineq1());
RUN(test_polysat::test_ineq2());
RUN(test_polysat::test_monot());