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

fixed typo in optimized unsat core plugin code

Browse source
This commit is contained in:
Bernhard Gleiss 2017-08-01 10:12:29 +02:00 • committed by Arie Gurfinkel
parent e315d063c5
commit bc3d8580c9
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/spacer/spacer_unsat_core_plugin.cpp
View file

@ -330,8 +330,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
{ {
SASSERT(!m_learner.is_a_marked(premise)); SASSERT(!m_learner.is_a_marked(premise));
// XXX AG: why is this condition is based on step and not on premise? if (m_learner.only_contains_symbols_b(m_learner.m.get_fact(premise)) && !m_learner.is_h_marked(premise))
if (m_learner.only_contains_symbols_b(m_learner.m.get_fact(step)) && !m_learner.is_h_marked(step))
{ {
rational coefficient; rational coefficient;
VERIFY(params[i].is_rational(coefficient)); VERIFY(params[i].is_rational(coefficient));