mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
build
This commit is contained in:
parent
0bd6725711
commit
d88f125818
|
@ -149,7 +149,7 @@ namespace sat {
|
|||
for (literal lit : m_solver.get_core())
|
||||
m_core.push_back(lit2ext(lit));
|
||||
if (is_sat == l_true) {
|
||||
TRACE("dual", display(s, tout); s.display(tout););
|
||||
TRACE("dual", display(tout); s.display(tout););
|
||||
IF_VERBOSE(0, verbose_stream() << "unexpected SAT\n");
|
||||
IF_VERBOSE(0, verbose_stream() << "assumptions: " << m_lits << "\n");
|
||||
IF_VERBOSE(0, display(verbose_stream()); s.display(verbose_stream()););
|
||||
|
|
|
@ -378,9 +378,7 @@ namespace smt {
|
|||
break;
|
||||
case l_true: {
|
||||
expr * true_arg = nullptr;
|
||||
unsigned num_args = n->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
expr * arg = n->get_arg(i);
|
||||
for (expr* arg : *n) {
|
||||
if (m_context.find_assignment(arg) == l_true) {
|
||||
if (is_relevant_core(arg))
|
||||
return;
|
||||
|
@ -402,9 +400,7 @@ namespace smt {
|
|||
switch (val) {
|
||||
case l_false: {
|
||||
expr * false_arg = nullptr;
|
||||
unsigned num_args = n->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
expr * arg = n->get_arg(i);
|
||||
for (expr* arg : *n) {
|
||||
if (m_context.find_assignment(arg) == l_false) {
|
||||
if (is_relevant_core(arg))
|
||||
return;
|
||||
|
|
Loading…
Reference in a new issue