mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix assertion, start addressing #1087 by using size_t

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-06-20 14:37:56 -07:00
parent 0ef14acf2e
commit e48e7ef7be
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_arith_aux.h
View file

@ -1412,7 +1412,7 @@ namespace smt {
<< "max gain: " << max_gain << "\n";);
SASSERT(max_gain.is_minus_one() || max_gain.is_one());
SASSERT(max_gain.is_minus_one() || !max_gain.is_neg());
SASSERT(min_gain.is_minus_one() || min_gain.is_one());
SASSERT(is_int(x) == min_gain.is_one());

2
src/smt/theory_str.cpp
View file

@ -9194,7 +9194,7 @@ namespace smt {
// ----------------------------------------------------------------------------------------
int len = atoi(lenStr.encode().c_str());
bool coverAll = false;
vector<int_vector, true, long long> options;
vector<int_vector, true, size_t> options;
int_vector base;
TRACE("str", tout