From b4d0216728dc3fdaa7f22ccf510e0b8652d4007b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Apr 2013 13:06:59 -0700 Subject: [PATCH] try to fix gcc build Signed-off-by: Nikolaj Bjorner --- src/smt/theory_horn_ineq_def.h | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/smt/theory_horn_ineq_def.h b/src/smt/theory_horn_ineq_def.h index 1fc51a86c..0b32c2c8d 100644 --- a/src/smt/theory_horn_ineq_def.h +++ b/src/smt/theory_horn_ineq_def.h @@ -797,10 +797,10 @@ namespace smt { template typename theory_horn_ineq::numeral theory_horn_ineq::mk_weight(bool is_real, bool is_strict, rational const& w) const { if (is_strict) { - return numeral(inf_numeral(w)) + (is_real?m_epsilon:numeral(1)); + return numeral(Ext::inf_numeral(w)) + (is_real?Ext::m_epsilon:numeral(1)); } else { - return numeral(inf_numeral(w)); + return numeral(Ext::inf_numeral(w)); } } @@ -1001,9 +1001,9 @@ namespace smt { th_var target = mk_var(ctx.mk_enode(n, false, false, true)); coeffs.push_back(std::make_pair(target, rational(-1))); - VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(w)), null_literal))); + VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(w)), null_literal))); negate(coeffs, w); - VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(w)), null_literal))); + VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(w)), null_literal))); return target; } @@ -1024,9 +1024,9 @@ namespace smt { // v = k: v <= k k <= v coeffs coeffs; coeffs.push_back(std::make_pair(v, rational(1))); - VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(r)), null_literal))); + VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(r)), null_literal))); coeffs.back().second.neg(); - VERIFY (m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(-r)), null_literal))); + VERIFY (m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(-r)), null_literal))); } return v; }