diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 679358932..f94de7eba 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -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());
 
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index d560a54a1..523e087f2 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -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