diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 203dd24d2..59f5521c5 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -683,7 +683,9 @@ void theory_diff_logic::set_neg_cycle_conflict() { vector params; if (get_manager().proofs_enabled()) { params.push_back(parameter(symbol("farkas"))); - params.resize(lits.size()+1, parameter(rational(1))); + for (unsigned i = 0; i <= lits.size(); ++i) { + params.push_back(parameter(rational(1))); + } } ctx.set_conflict(