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

Fixed signed/unsigned comparison warnings

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-05-31 18:35:06 +01:00
parent a7d5bb7b36
commit 4f0a87299c
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/theory_str.cpp
View file

@ -5563,7 +5563,7 @@ namespace smt {
if (arg0VecSize > 0 && arg1VecSize > 0 && u.str.is_string(arg0_grdItor->first[arg0VecSize - 1]) && u.str.is_string(arg1_grdItor->first[0])) {
ndVec.pop_back();
ndVec.push_back(mk_concat(arg0_grdItor->first[arg0VecSize - 1], arg1_grdItor->first[0]));
for (int i = 1; i < arg1VecSize; i++) {
for (size_t i = 1; i < arg1VecSize; i++) {
ndVec.push_back(arg1_grdItor->first[i]);
}
} else {
@ -5666,7 +5666,7 @@ namespace smt {
if (subStrCnt == 1) {
zstring subStrVal;
if (u.str.is_string(subStrVec[0], subStrVal)) {
for (int i = 0; i < strCnt; i++) {
for (size_t i = 0; i < strCnt; i++) {
zstring strVal;
if (u.str.is_string(strVec[i], strVal)) {
if (strVal.contains(subStrVal)) {
@ -5675,7 +5675,7 @@ namespace smt {
}
}
} else {
for (int i = 0; i < strCnt; i++) {
for (size_t i = 0; i < strCnt; i++) {
if (strVec[i] == subStrVec[0]) {
return true;
}
@ -5683,7 +5683,7 @@ namespace smt {
}
return false;
} else {
for (int i = 0; i <= (strCnt - subStrCnt); i++) {
for (size_t i = 0; i <= (strCnt - subStrCnt); i++) {
// The first node in subStrVect should be
// * constant: a suffix of a note in strVec[i]
// * variable:
@ -5712,7 +5712,7 @@ namespace smt {
// middle nodes
bool midNodesOK = true;
for (int j = 1; j < subStrCnt - 1; j++) {
for (size_t j = 1; j < subStrCnt - 1; j++) {
if (subStrVec[j] != strVec[i + j]) {
midNodesOK = false;
break;