one other warning (from Michael)

vprover · Nov 30, 2021 · 1bec8ad · 1bec8ad
1 parent 3be9154
commit 1bec8ad
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/SAT/Z3Interfacing.hpp b/SAT/Z3Interfacing.hpp
@@ -169,7 +169,7 @@ class Z3Interfacing : public PrimitiveProofRecordingSATSolver
         return true;
 
       // compare sort arguments
-      for(int i = 0; i < l.forSorts->numTypeArguments(); i++)
+      for(unsigned i = 0; i < l.forSorts->numTypeArguments(); i++)
         // sorts are perfectly shared
         if(!l.forSorts->nthArgument(i)->sameContent(r.forSorts->nthArgument(i)))
           return false;
@@ -185,7 +185,7 @@ class Z3Interfacing : public PrimitiveProofRecordingSATSolver
           : env.signature->getFunction(self.id)->name()
       );
       if(self.forSorts)
-        for(int i = 0; i < self.forSorts->numTypeArguments(); i++)
+        for(unsigned i = 0; i < self.forSorts->numTypeArguments(); i++)
           out << " " << self.forSorts->nthArgument(i)->toString();
       return out;
     }
@@ -281,7 +281,7 @@ namespace std {
       size_t operator()(SAT::Z3Interfacing::FuncOrPredId const& self) {
         unsigned hash = Lib::HashUtils::combine(self.id, self.isPredicate);
         if(self.forSorts)
-          for(int i = 0; i < self.forSorts->numTypeArguments(); i++)
+          for(unsigned i = 0; i < self.forSorts->numTypeArguments(); i++)
             hash = Lib::HashUtils::combine(hash, self.forSorts->nthArgument(i)->content());
         return hash;
       }