Skip to content

Commit

Permalink
don't use FM until understood better
Browse files Browse the repository at this point in the history
  • Loading branch information
Dejan Jovanovic authored and BrunoDutertre committed May 24, 2020
1 parent 8722b31 commit 4e883bf
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/mcsat/nra/nra_plugin_explain.c
Original file line number Diff line number Diff line change
Expand Up @@ -1018,7 +1018,7 @@ void nra_plugin_explain_conflict(nra_plugin_t* nra, const int_mset_t* pos, const
}

// Check if there is a simple Fourier-Motzkin explanation
if (core->size == 2 && lemma_reasons->size == 0) {
if (false && core->size == 2 && lemma_reasons->size == 0) {
variable_t c0_var = core->data[0];
variable_t c1_var = core->data[1];
bool c0_negated = !constraint_get_value(nra->ctx->trail, pos, neg, c0_var);
Expand Down

0 comments on commit 4e883bf

Please sign in to comment.