mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

minor

Browse source
This commit is contained in:
Jakob Rath 2022-11-09 17:00:27 +01:00
parent abc4cc5295
commit 4b146a61ff
1 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/test/polysat.cpp
View file

@ -172,7 +172,7 @@ namespace polysat {
char const* msg = e.msg(); char const* msg = e.msg();
if (!msg) if (!msg)
msg = "(unknown z3_exception)"; msg = "(unknown z3_exception)";
std::cout << "\n\nEXCEPTION during test: " << m_name << ": " << msg << "\n\n"; std::cout << "\n\nEXCEPTION (z3_exception) during test: " << m_name << ": " << msg << "\n\n";
m_record->m_result = test_result::error; m_record->m_result = test_result::error;
m_record->m_error_message = msg; m_record->m_error_message = msg;
if (!collect_test_records) if (!collect_test_records)
@ -183,7 +183,7 @@ namespace polysat {
char const* msg = e.what(); char const* msg = e.what();
if (!msg) if (!msg)
msg = "(unknown std::exception)"; msg = "(unknown std::exception)";
std::cout << "\n\nEXCEPTION during test: " << m_name << ": " << msg << "\n\n"; std::cout << "\n\nEXCEPTION (std::exception) during test: " << m_name << ": " << msg << "\n\n";
m_record->m_result = test_result::error; m_record->m_result = test_result::error;
m_record->m_error_message = msg; m_record->m_error_message = msg;
if (!collect_test_records) if (!collect_test_records)
@ -192,7 +192,7 @@ namespace polysat {
catch(...) { catch(...) {
m_record->end = test_record::clock_t::now(); m_record->end = test_record::clock_t::now();
char const* msg = "(unknown throwable)"; char const* msg = "(unknown throwable)";
std::cout << "\n\nEXCEPTION during test: " << m_name << ": " << msg << "\n\n"; std::cout << "\n\nEXCEPTION (unknown throwable) during test: " << m_name << ": " << msg << "\n\n";
m_record->m_result = test_result::error; m_record->m_result = test_result::error;
m_record->m_error_message = msg; m_record->m_error_message = msg;
if (!collect_test_records) if (!collect_test_records)
@ -206,6 +206,8 @@ namespace polysat {
void expect_unsat() { void expect_unsat() {
SASSERT_EQ(m_record->m_expected, l_undef); SASSERT_EQ(m_record->m_expected, l_undef);
m_record->m_expected = l_false; m_record->m_expected = l_false;
if (m_record->m_result == test_result::error)
return;
if (m_last_result != l_false && m_last_result != l_undef) { if (m_last_result != l_false && m_last_result != l_undef) {
m_record->m_result = test_result::wrong_answer; m_record->m_result = test_result::wrong_answer;
LOG_H1("FAIL: " << m_name << ": expected UNSAT, got " << m_last_result << "!"); LOG_H1("FAIL: " << m_name << ": expected UNSAT, got " << m_last_result << "!");
@ -217,6 +219,8 @@ namespace polysat {
void expect_sat(std::vector<std::pair<dd::pdd, unsigned>> const& expected_assignment = {}) { void expect_sat(std::vector<std::pair<dd::pdd, unsigned>> const& expected_assignment = {}) {
SASSERT_EQ(m_record->m_expected, l_undef); SASSERT_EQ(m_record->m_expected, l_undef);
m_record->m_expected = l_true; m_record->m_expected = l_true;
if (m_record->m_result == test_result::error)
return;
if (m_last_result == l_true) { if (m_last_result == l_true) {
for (auto const& p : expected_assignment) { for (auto const& p : expected_assignment) {
auto const& v_pdd = p.first; auto const& v_pdd = p.first;
@ -438,8 +442,6 @@ namespace polysat {
s.add_ule(w, u); s.add_ule(w, u);
s.check(); s.check();
s.expect_sat(); s.expect_sat();
SASSERT_EQ(s.get_value(u.var()), s.get_value(v.var()));
SASSERT_EQ(s.get_value(u.var()), s.get_value(w.var()));
} }
// Unsatisfiable // Unsatisfiable
@ -1565,6 +1567,8 @@ void tst_polysat() {
return; return;
#endif #endif
collect_test_records = true;
if (collect_test_records) { if (collect_test_records) {
set_default_debug_action(debug_action::throw_exception); set_default_debug_action(debug_action::throw_exception);
set_log_enabled(false); set_log_enabled(false);