diff --git a/deps/k_release b/deps/k_release
index 452ca39512..6bf1436f90 100644
--- a/deps/k_release
+++ b/deps/k_release
@@ -1 +1 @@
-6.0.87
+6.0.121
diff --git a/test/imp/max-symbolic.imp.out.golden b/test/imp/max-symbolic.imp.out.golden
index 4890297523..d176363edf 100644
--- a/test/imp/max-symbolic.imp.out.golden
+++ b/test/imp/max-symbolic.imp.out.golden
@@ -3,7 +3,7 @@
         .
       </k>
       <state>
-        max |-> ?_I:Int
+        max |-> ?_I0:Int
         x |-> ?_I:Int
         y |-> ?_I0:Int
         z |-> ?_I1:Int
@@ -13,13 +13,13 @@
     {
       false
     #Equals
-      ?_I:Int <=Int ?_I0:Int
+      ?_I0:Int <=Int ?_I1:Int
     }
   #And
     {
-      false
+      true
     #Equals
-      ?_I:Int <=Int ?_I1:Int
+      ?_I:Int <=Int ?_I0:Int
     }
 #Or
     <T>
@@ -27,7 +27,7 @@
         .
       </k>
       <state>
-        max |-> ?_I0:Int
+        max |-> ?_I1:Int
         x |-> ?_I:Int
         y |-> ?_I0:Int
         z |-> ?_I1:Int
@@ -37,13 +37,13 @@
     {
       false
     #Equals
-      ?_I0:Int <=Int ?_I1:Int
+      ?_I:Int <=Int ?_I0:Int
     }
   #And
     {
       true
     #Equals
-      ?_I:Int <=Int ?_I0:Int
+      ?_I:Int <=Int ?_I1:Int
     }
 #Or
     <T>
@@ -59,15 +59,15 @@
     </T>
   #And
     {
-      false
+      true
     #Equals
-      ?_I:Int <=Int ?_I0:Int
+      ?_I0:Int <=Int ?_I1:Int
     }
   #And
     {
       true
     #Equals
-      ?_I:Int <=Int ?_I1:Int
+      ?_I:Int <=Int ?_I0:Int
     }
 #Or
     <T>
@@ -75,7 +75,7 @@
         .
       </k>
       <state>
-        max |-> ?_I1:Int
+        max |-> ?_I:Int
         x |-> ?_I:Int
         y |-> ?_I0:Int
         z |-> ?_I1:Int
@@ -83,13 +83,13 @@
     </T>
   #And
     {
-      true
+      false
     #Equals
-      ?_I0:Int <=Int ?_I1:Int
+      ?_I:Int <=Int ?_I0:Int
     }
   #And
     {
-      true
+      false
     #Equals
-      ?_I:Int <=Int ?_I0:Int
+      ?_I:Int <=Int ?_I1:Int
     }
diff --git a/test/issue-2010/1.test.out.golden b/test/issue-2010/1.test.out.golden
index f2d06cfce3..9b22e92fcd 100644
--- a/test/issue-2010/1.test.out.golden
+++ b/test/issue-2010/1.test.out.golden
@@ -1,19 +1,19 @@
     <k>
-      true ~> .
+      I:Int ~> .
     </k>
   #And
     {
-      None
+      Some I:Int
     #Equals
       f ( )
     }
 #Or
     <k>
-      I:Int ~> .
+      true ~> .
     </k>
   #And
     {
-      Some I:Int
+      None
     #Equals
       f ( )
     }
diff --git a/test/smt-none/program.test.out.golden b/test/smt-none/program.test.out.golden
index 1e1d8ab5aa..e2f42e4b3c 100644
--- a/test/smt-none/program.test.out.golden
+++ b/test/smt-none/program.test.out.golden
@@ -1,13 +1,3 @@
-    <k>
-      .
-    </k>
-  #And
-    {
-      ?T1:Type
-    #Equals
-      ?T2:Type
-    }
-#Or
     #Not ( {
       ?T1:Type
     #Equals
@@ -17,3 +7,13 @@
     <k>
       ?T1:Type = ?T2:Type ~> .
     </k>
+#Or
+    <k>
+      .
+    </k>
+  #And
+    {
+      ?T1:Type
+    #Equals
+      ?T2:Type
+    }