for better debugging

Author: daejunpark

API/src/main/java/org/kframework/EquivChecker.java

@@ -126,7 +126,9 @@ public static java.util.List<Set<SyncNode>> getNextSyncNodes(
 
         queue.add(currSyncNode.currSyncNode);
 
+        int steps = 0;
         while (!queue.isEmpty()) {
+            ++steps;
             for (ConstrainedTerm curr : queue) {
 
                 java.util.List<ConstrainedTerm> nexts = rewriter.fastComputeRewriteStep(curr, false, true, true);

API/src/main/java/org/kframework/Kapi.java

@@ -311,6 +311,8 @@ public static Info getInfo(CompiledDefinition compiledDef, String proofFile, Str
 
         //// setting options
 
+        globalOptions.debug = true;
+
         krunOptions.experimental.prove = proofFile;
         krunOptions.experimental.smt.smtPrelude = prelude;
 

java-backend/src/main/java/org/kframework/backend/java/symbolic/FastRuleMatcher.java

@@ -326,7 +326,11 @@ private BitSet match(Term subject, Term pattern, BitSet ruleMask, scala.collecti
             return unifyMapModuloPatternFolding((BuiltinMap) subject, (BuiltinMap) pattern, ruleMask, path);
         } else if (subject instanceof Token && pattern instanceof Token) {
             // TODO: make tokens unique?
-            return subject.equals(pattern) ? ruleMask : empty;
+            if (subject.equals(pattern)) {
+                return ruleMask;
+            } else {
+                return empty;
+            }
         } else if (subject instanceof BuiltinSet && pattern instanceof BuiltinSet) {
             return subject.equals(pattern) ? ruleMask : empty;
         } else {