diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py
index c69028757..8039be69a 100644
--- a/scripts/mk_nuget_task.py
+++ b/scripts/mk_nuget_task.py
@@ -25,6 +25,7 @@ def mk_dir(d):
 os_info = {"z64-ubuntu-14" : ('so', 'ubuntu.14.04-x64'),
            'ubuntu-18' : ('so', 'ubuntu-x64'),
            'ubuntu-20' : ('so', 'ubuntu-x64'),
+           'glibc-2.31' : ('so', 'glibc-x64'),
            'x64-win' : ('dll', 'win-x64'),
            'x86-win' : ('dll', 'win-x86'),
            'osx' : ('dylib', 'macos'),
@@ -35,6 +36,7 @@ def classify_package(f):
         if os_name in f:
             ext, dst = os_info[os_name]
             return os_name, f[:-4], ext, dst
+    print("Could not classify", f)
     return None
 
 def replace(src, dst):
@@ -49,9 +51,7 @@ def unpack(packages, symbols):
     # +- runtimes
     #    +- win-x64
     #    +- win-x86
-    #    +- ubuntu.16.04-x64
-    #    +- ubuntu.14.04-x64
-    #    +- debian.8-x64
+    #    +- ubuntu-x64
     #    +- macos
     # +
     tmp = "tmp" if not symbols else "tmpsym"
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index b4e7ded1b..c534b6726 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -1656,10 +1656,9 @@ namespace qe {
                 return false;
             }
 
-            unsigned_vector& vec = m_partition.back();;
-            for (unsigned i = 0; i < vec.size(); ++i) {
-                vars.push_back(m_current->free_var(vec[i]));
-            }
+            unsigned_vector& vec = m_partition.back();
+            for (auto v : vec)
+                vars.push_back(m_current->free_var(v));
             m_partition.pop_back();
             return true;
         }
diff --git a/src/qe/qe_array_plugin.cpp b/src/qe/qe_array_plugin.cpp
index 96ddc8e2c..8b379abe2 100644
--- a/src/qe/qe_array_plugin.cpp
+++ b/src/qe/qe_array_plugin.cpp
@@ -264,21 +264,16 @@ namespace qe {
         bool is_array_app_of(app* a, unsigned& idx, expr* t, decl_kind k, vector<ptr_vector<expr> >& args) {
             if (m_ctx.is_var(a, idx)) {
                 contains_app& contains_v = m_ctx.contains(idx);
-                if (args.empty() || contains_v(t)) {
+                if (args.empty() || contains_v(t)) 
                     return false;
-                }
-                for (unsigned i = 0; i < args.size(); ++i) {
-                    for (unsigned j = 0; j < args[i].size(); ++j) {
-                        if (contains_v(args[i][j])) {
+                for (auto const& vs : args)
+                    for (auto v : vs)
+                        if (contains_v(v))
                             return false;
-                        }
-                    }
-                }
                 return true;
             }            
-            if (!is_app_of(a, m_fid, k)) {
+            if (!is_app_of(a, m_fid, k)) 
                 return false;
-            }
             args.push_back(ptr_vector<expr>());
             for (unsigned i = 1; i < a->get_num_args(); ++i) {
                 args.back().push_back(a->get_arg(i));