mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

fix build warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-05-15 15:56:21 +01:00
parent 93f55605a8
commit e6b8af402f
2 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/opt/hitting_sets.cpp
View file

@ -122,7 +122,7 @@ namespace opt {
bool m_enable_simplex; bool m_enable_simplex;
struct compare_scores { struct compare_scores {
imp* m_imp; imp* m_imp;
compare_scores(imp* i):m_imp(i) {} compare_scores():m_imp(0) {}
bool operator()(int v1, int v2) const { bool operator()(int v1, int v2) const {
return m_imp->m_scored_weights[v1] > m_imp->m_scored_weights[v2]; return m_imp->m_scored_weights[v1] > m_imp->m_scored_weights[v2];
} }
@ -154,10 +154,10 @@ namespace opt {
m_scope_lvl(0), m_scope_lvl(0),
m_conflict_j(justification(justification::AXIOM)), m_conflict_j(justification(justification::AXIOM)),
m_inconsistent(false), m_inconsistent(false),
m_compare_scores(this), m_compare_scores(),
m_heap(0, m_compare_scores) { m_heap(0, m_compare_scores) {
m_enable_simplex = true; m_enable_simplex = true;
m_compare_scores.m_imp = this;
} }
~imp() { ~imp() {
for (unsigned i = 0; i < m_T.size(); ++i) { for (unsigned i = 0; i < m_T.size(); ++i) {

2
src/util/mpff.cpp
View file

@ -255,7 +255,7 @@ void mpff_manager::set(mpff & n, int64 v) {
} }
else { else {
if (v < 0) { if (v < 0) {
set(n, -static_cast<uint64>(v)); set(n, 1 + static_cast<uint64>(-(1+v)));
n.m_sign = 1; n.m_sign = 1;
} }
else { else {