diff --git a/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.handler.test/models/jetbrains/mps/lang/typesystem2/samplechecker/handle/test/util.mps b/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.handler.test/models/jetbrains/mps/lang/typesystem2/samplechecker/handle/test/util.mps
index f471a86b..dba186e5 100644
--- a/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.handler.test/models/jetbrains/mps/lang/typesystem2/samplechecker/handle/test/util.mps
+++ b/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.handler.test/models/jetbrains/mps/lang/typesystem2/samplechecker/handle/test/util.mps
@@ -3959,7 +3959,7 @@
               <property role="TrG5h" value="success" />
               <node concept="10P_77" id="3KV3FXk2bq5" role="1tU5fm" />
               <node concept="2YIFZM" id="3KV3FXk2bPE" role="33vP2m">
-                <ref role="37wK5l" to="4r4j:3KV3FXk1fGe" resolve="findSubtypePath" />
+                <ref role="37wK5l" to="4r4j:3KV3FXk1fGe" resolve="findSubtypingPath" />
                 <ref role="1Pybhc" to="4r4j:3KV3FXk1fjd" resolve="SubtypePathSolver" />
                 <node concept="37vLTw" id="3KV3FXk2bPF" role="37wK5m">
                   <ref role="3cqZAo" node="3KV3FXk2bpY" resolve="var" />
@@ -4010,31 +4010,11 @@
                 <node concept="1oi5ST" id="3KV3FXk2bqq" role="1oi0x0">
                   <property role="TrG5h" value="list" />
                   <node concept="KCUsM" id="3KV3FXk2bqr" role="1oi5TL">
-                    <node concept="1oi5UN" id="3KV3FXk2bqs" role="KCVpo">
-                      <node concept="1oi5Wm" id="3KV3FXk2bqt" role="1ojpOf">
+                    <node concept="1oi5UN" id="3KV3FXk2iIU" role="KCVpo">
+                      <node concept="1oi5Wm" id="3KV3FXk2iIV" role="1ojpOf">
                         <property role="TrG5h" value="concept" />
-                        <node concept="1oi5XN" id="3KV3FXk2bqu" role="1oi5zu">
-                          <property role="1oi5yK" value="ClassifierType" />
-                        </node>
-                      </node>
-                      <node concept="1oi5Wm" id="3KV3FXk2bqv" role="1ojpOf">
-                        <property role="TrG5h" value="classifier" />
-                        <node concept="1oi5XN" id="3KV3FXk2bqw" role="1oi5zu">
-                          <property role="1oi5yK" value="Serializable" />
-                        </node>
-                      </node>
-                    </node>
-                    <node concept="1oi5UN" id="3KV3FXk2bRR" role="KCVpo">
-                      <node concept="1oi5Wm" id="3KV3FXk2bRS" role="1ojpOf">
-                        <property role="TrG5h" value="concept" />
-                        <node concept="1oi5XN" id="3KV3FXk2bRT" role="1oi5zu">
-                          <property role="1oi5yK" value="ClassifierType" />
-                        </node>
-                      </node>
-                      <node concept="1oi5Wm" id="3KV3FXk2bRU" role="1ojpOf">
-                        <property role="TrG5h" value="classifier" />
-                        <node concept="1oi5XN" id="3KV3FXk2bRV" role="1oi5zu">
-                          <property role="1oi5yK" value="Number" />
+                        <node concept="1oi5XN" id="3KV3FXk2iIW" role="1oi5zu">
+                          <property role="1oi5yK" value="LongType" />
                         </node>
                       </node>
                     </node>
@@ -4052,11 +4032,31 @@
                         </node>
                       </node>
                     </node>
-                    <node concept="1oi5UN" id="3KV3FXk2iIU" role="KCVpo">
-                      <node concept="1oi5Wm" id="3KV3FXk2iIV" role="1ojpOf">
+                    <node concept="1oi5UN" id="3KV3FXk2bRR" role="KCVpo">
+                      <node concept="1oi5Wm" id="3KV3FXk2bRS" role="1ojpOf">
                         <property role="TrG5h" value="concept" />
-                        <node concept="1oi5XN" id="3KV3FXk2iIW" role="1oi5zu">
-                          <property role="1oi5yK" value="LongType" />
+                        <node concept="1oi5XN" id="3KV3FXk2bRT" role="1oi5zu">
+                          <property role="1oi5yK" value="ClassifierType" />
+                        </node>
+                      </node>
+                      <node concept="1oi5Wm" id="3KV3FXk2bRU" role="1ojpOf">
+                        <property role="TrG5h" value="classifier" />
+                        <node concept="1oi5XN" id="3KV3FXk2bRV" role="1oi5zu">
+                          <property role="1oi5yK" value="Number" />
+                        </node>
+                      </node>
+                    </node>
+                    <node concept="1oi5UN" id="3KV3FXk2bqs" role="KCVpo">
+                      <node concept="1oi5Wm" id="3KV3FXk2bqt" role="1ojpOf">
+                        <property role="TrG5h" value="concept" />
+                        <node concept="1oi5XN" id="3KV3FXk2bqu" role="1oi5zu">
+                          <property role="1oi5yK" value="ClassifierType" />
+                        </node>
+                      </node>
+                      <node concept="1oi5Wm" id="3KV3FXk2bqv" role="1ojpOf">
+                        <property role="TrG5h" value="classifier" />
+                        <node concept="1oi5XN" id="3KV3FXk2bqw" role="1oi5zu">
+                          <property role="1oi5yK" value="Serializable" />
                         </node>
                       </node>
                     </node>
diff --git a/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.handler.util/models/jetbrains/mps/lang/typesystem2/samplechecker/handle/util.mps b/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.handler.util/models/jetbrains/mps/lang/typesystem2/samplechecker/handle/util.mps
index 814088a6..b54d1361 100644
--- a/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.handler.util/models/jetbrains/mps/lang/typesystem2/samplechecker/handle/util.mps
+++ b/languages/jetbrains.mps.lang.typesystem2/sandbox/jetbrains.mps.lang.typesystem2.samplechecker.handler.util/models/jetbrains/mps/lang/typesystem2/samplechecker/handle/util.mps
@@ -390,12 +390,21 @@
             </node>
           </node>
           <node concept="3clFbS" id="3KV3FXjZMUD" role="3clFbx">
+            <node concept="3clFbF" id="5_6ImQZ8n1E" role="3cqZAp">
+              <node concept="2YIFZM" id="5_6ImQZ8n8A" role="3clFbG">
+                <ref role="37wK5l" to="yg8f:5_6ImQZ8ja0" resolve="fail" />
+                <ref role="1Pybhc" to="yg8f:5_6ImQZ8j9D" resolve="SolverUtil" />
+                <node concept="Xl_RD" id="5_6ImQZ8nfH" role="37wK5m">
+                  <property role="Xl_RC" value="could not find LUB" />
+                </node>
+              </node>
+            </node>
             <node concept="3cpWs6" id="3KV3FXjZMUE" role="3cqZAp">
               <node concept="3clFbT" id="3KV3FXjZMUF" role="3cqZAk">
                 <property role="3clFbU" value="false" />
               </node>
             </node>
-            <node concept="3clFbH" id="3KV3FXk0uiD" role="3cqZAp" />
+            <node concept="3clFbH" id="5_6ImQZ8n8S" role="3cqZAp" />
           </node>
           <node concept="9aQIb" id="3KV3FXk0tjw" role="9aQIa">
             <node concept="3clFbS" id="3KV3FXk0tjx" role="9aQI4">
@@ -1630,7 +1639,7 @@
     <property role="TrG5h" value="SubtypePathSolver" />
     <node concept="2tJIrI" id="3KV3FXk1fFS" role="jymVt" />
     <node concept="2YIFZL" id="3KV3FXk1fGe" role="jymVt">
-      <property role="TrG5h" value="findSubtypePath" />
+      <property role="TrG5h" value="findSubtypingPath" />
       <node concept="37vLTG" id="3KV3FXk1fGz" role="3clF46">
         <property role="TrG5h" value="result" />
         <node concept="3uibUv" id="3KV3FXk1fGJ" role="1tU5fm">
@@ -1763,8 +1772,17 @@
         <node concept="3clFbH" id="3KV3FXk1jbh" role="3cqZAp" />
         <node concept="3clFbJ" id="3KV3FXk1kIP" role="3cqZAp">
           <node concept="3clFbS" id="3KV3FXk1kIR" role="3clFbx">
-            <node concept="3cpWs6" id="3KV3FXk1lze" role="3cqZAp">
-              <node concept="3clFbT" id="3KV3FXk1lBH" role="3cqZAk">
+            <node concept="3clFbF" id="5_6ImQZ8rNY" role="3cqZAp">
+              <node concept="2YIFZM" id="5_6ImQZ8rNZ" role="3clFbG">
+                <ref role="1Pybhc" to="yg8f:5_6ImQZ8j9D" resolve="SolverUtil" />
+                <ref role="37wK5l" to="yg8f:5_6ImQZ8ja0" resolve="fail" />
+                <node concept="Xl_RD" id="5_6ImQZ8rO0" role="37wK5m">
+                  <property role="Xl_RC" value="could not find subtyping path" />
+                </node>
+              </node>
+            </node>
+            <node concept="3cpWs6" id="5_6ImQZ8rO1" role="3cqZAp">
+              <node concept="3clFbT" id="5_6ImQZ8rO2" role="3cqZAk">
                 <property role="3clFbU" value="false" />
               </node>
             </node>
@@ -1829,7 +1847,7 @@
       <node concept="P$JXv" id="3KV3FXk1Zlo" role="lGtFl">
         <node concept="TZ5HA" id="3KV3FXk1Zlp" role="TZ5H$">
           <node concept="1dT_AC" id="3KV3FXk1Zlq" role="1dT_Ay">
-            <property role="1dT_AB" value="Finds the shortest path among those specified in " />
+            <property role="1dT_AB" value="Find the shortest path among those specified in " />
           </node>
           <node concept="1dT_AA" id="3KV3FXk1ZsS" role="1dT_Ay">
             <node concept="VVOAv" id="3KV3FXk1ZsY" role="qph3F">
@@ -1858,7 +1876,7 @@
             </node>
           </node>
           <node concept="1dT_AC" id="3KV3FXk1Zts" role="1dT_Ay">
-            <property role="1dT_AB" value="." />
+            <property role="1dT_AB" value=". Then reverse the path so that it becomes a supertypes path." />
           </node>
         </node>
         <node concept="TZ5HA" id="3KV3FXk1ZtF" role="TZ5H$">
@@ -1938,7 +1956,12 @@
             </node>
           </node>
           <node concept="1dT_AC" id="3KV3FXk28AY" role="1dT_Ay">
-            <property role="1dT_AB" value=" contains the shortest path originating at " />
+            <property role="1dT_AB" value=" contains the shortest path originating at the type in question" />
+          </node>
+        </node>
+        <node concept="TZ5HA" id="5_6ImQZlA11" role="TZ5H$">
+          <node concept="1dT_AC" id="5_6ImQZlA12" role="1dT_Ay">
+            <property role="1dT_AB" value="and ending at " />
           </node>
           <node concept="1dT_AA" id="3KV3FXk28Ce" role="1dT_Ay">
             <node concept="VVOAv" id="3KV3FXk28Cu" role="qph3F">
@@ -2188,6 +2211,15 @@
             <node concept="3clFbH" id="3KV3FXk1KHA" role="3cqZAp" />
             <node concept="3clFbJ" id="3KV3FXk1R1l" role="3cqZAp">
               <node concept="3clFbS" id="3KV3FXk1R1n" role="3clFbx">
+                <node concept="3clFbF" id="5_6ImQZl_Vo" role="3cqZAp">
+                  <node concept="2YIFZM" id="5_6ImQZl_Y0" role="3clFbG">
+                    <ref role="37wK5l" to="33ny:~Collections.reverse(java.util.List):void" resolve="reverse" />
+                    <ref role="1Pybhc" to="33ny:~Collections" resolve="Collections" />
+                    <node concept="37vLTw" id="5_6ImQZl_Z7" role="37wK5m">
+                      <ref role="3cqZAo" node="3KV3FXk1Lsq" resolve="candidatePath" />
+                    </node>
+                  </node>
+                </node>
                 <node concept="3clFbF" id="3KV3FXk1U$D" role="3cqZAp">
                   <node concept="37vLTI" id="3KV3FXk1UFS" role="3clFbG">
                     <node concept="37vLTw" id="3KV3FXk1UH3" role="37vLTx">
diff --git a/languages/jetbrains.mps.logic/runtime/models/jetbrains/mps/logic/builtin.mps b/languages/jetbrains.mps.logic/runtime/models/jetbrains/mps/logic/builtin.mps
index 40689bee..c5ae7764 100644
--- a/languages/jetbrains.mps.logic/runtime/models/jetbrains/mps/logic/builtin.mps
+++ b/languages/jetbrains.mps.logic/runtime/models/jetbrains/mps/logic/builtin.mps
@@ -11,6 +11,7 @@
     <import index="oy3s" ref="r:a6030cee-34eb-4503-b1bf-015fe5cd8c1a(jetbrains.mps.logic.builtin.unification)" />
     <import index="yt73" ref="7526e0cf-1ce7-46f8-a555-9eca1e06c23b/java:jetbrains.mps.unification(jetbrains.mps.unification.tree/)" />
     <import index="wyt6" ref="6354ebe7-c22a-4a0f-ac54-50b52ab9b065/java:java.lang(JDK/)" />
+    <import index="eifs" ref="b984ee52-f34d-4b6d-8812-866c1d3eae31/java:runtime(jetbrains.mps.jchr.runtime/)" />
   </imports>
   <registry>
     <language id="f3061a53-9226-4cc5-a443-f952ceaf5816" name="jetbrains.mps.baseLanguage">
@@ -124,6 +125,7 @@
         <child id="1068581242865" name="localVariableDeclaration" index="3cpWs9" />
       </concept>
       <concept id="1068581242863" name="jetbrains.mps.baseLanguage.structure.LocalVariableDeclaration" flags="nr" index="3cpWsn" />
+      <concept id="1068581517677" name="jetbrains.mps.baseLanguage.structure.VoidType" flags="in" index="3cqZAl" />
       <concept id="1081506773034" name="jetbrains.mps.baseLanguage.structure.LessThanExpression" flags="nn" index="3eOVzh" />
       <concept id="1204053956946" name="jetbrains.mps.baseLanguage.structure.IMethodCall" flags="ng" index="1ndlxa">
         <reference id="1068499141037" name="baseMethodDeclaration" index="37wK5l" />
@@ -1213,5 +1215,31 @@
     <node concept="2tJIrI" id="46l0wJhtOHe" role="jymVt" />
     <node concept="3Tm1VV" id="46l0wJhtODA" role="1B3o_S" />
   </node>
+  <node concept="312cEu" id="5_6ImQZ8j9D">
+    <property role="TrG5h" value="SolverUtil" />
+    <node concept="2tJIrI" id="5_6ImQZ8j9N" role="jymVt" />
+    <node concept="2YIFZL" id="5_6ImQZ8ja0" role="jymVt">
+      <property role="TrG5h" value="fail" />
+      <node concept="3cqZAl" id="5_6ImQZ8ja2" role="3clF45" />
+      <node concept="3Tm1VV" id="5_6ImQZ8ja3" role="1B3o_S" />
+      <node concept="3clFbS" id="5_6ImQZ8ja4" role="3clF47">
+        <node concept="YS8fn" id="5_6ImQZ8jaz" role="3cqZAp">
+          <node concept="2ShNRf" id="5_6ImQZ8jaX" role="YScLw">
+            <node concept="1pGfFk" id="5_6ImQZ8l0Z" role="2ShVmc">
+              <ref role="37wK5l" to="eifs:~FailureException.&lt;init&gt;(java.lang.String)" resolve="FailureException" />
+              <node concept="37vLTw" id="5_6ImQZ8l2j" role="37wK5m">
+                <ref role="3cqZAo" node="5_6ImQZ8l1u" resolve="message" />
+              </node>
+            </node>
+          </node>
+        </node>
+      </node>
+      <node concept="37vLTG" id="5_6ImQZ8l1u" role="3clF46">
+        <property role="TrG5h" value="message" />
+        <node concept="17QB3L" id="5_6ImQZ8l1t" role="1tU5fm" />
+      </node>
+    </node>
+    <node concept="3Tm1VV" id="5_6ImQZ8j9E" role="1B3o_S" />
+  </node>
 </model>