mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-06 01:43:49 -08:00
parent 5d772c1eb1
commit b2a6c30100
2 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/nex.h
View file

@ -208,12 +208,12 @@ public:
nex_mul() : m_coeff(1) {}
nex_mul(rational const& c, vector<nex_pow> const& args) : m_coeff(c), m_children(args) {}
const rational& coeff() const { return m_coeff; }
const rational& coeff() const override { return m_coeff; }
unsigned size() const override { return m_children.size(); }
expr_type type() const override { return expr_type::MUL; }
// A monomial is 'pure' if does not have a numeric coefficient.
bool is_pure_monomial() const { return size() == 0 || !m_children[0].e()->is_scalar(); }
bool is_pure_monomial() const override { return size() == 0 || !m_children[0].e()->is_scalar(); }
std::ostream & print(std::ostream& out) const override {
bool first = true;
@ -236,7 +236,7 @@ public:
const nex_pow* begin() const { return m_children.begin(); }
const nex_pow* end() const { return m_children.end(); }
bool contains(lpvar j) const {
bool contains(lpvar j) const override {
for (const nex_pow& c : *this) {
if (c.e()->contains(j))
return true;
@ -269,7 +269,7 @@ public:
return get_degree() < 2; // todo: make it more efficient
}
bool all_factors_are_elementary() const;
bool all_factors_are_elementary() const override;
// #ifdef Z3DEBUG
// virtual void sort() {

3
src/smt/theory_lra.cpp
View file

@ -2364,13 +2364,12 @@ public:
if (!should_propagate())
return;
local_bound_propagator bp(*this);
unsigned num_changed = lp().num_changed_bounds();
unsigned props = m_stats.m_bound_propagations1;
lp().propagate_bounds_for_touched_rows(bp);
if (m.canceled()) {
return;
}
unsigned props = m_stats.m_bound_propagations1;
if (is_infeasible()) {
get_infeasibility_explanation_and_set_conflict();