Fixed seq indexing manual check.

sireum · Mar 20, 2024 · 6f432c8 · 6f432c8
1 parent bd705f9
commit 6f432c8
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala
@@ -993,9 +993,9 @@ import Util._
         }
         return s0
       }
-      if (normPCs.contains(loHiCondExp)) {
+      if (normPCs.contains(th.normalizeExp(loHiCondExp))) {
         return accept(loHiCondExp.prettyST, "is in")
-      } else if (normPCs.contains(th.normalizeExp(loCondExp)) && normPCs.contains(hiCondExp)) {
+      } else if (normPCs.contains(th.normalizeExp(loCondExp)) && normPCs.contains(th.normalizeExp(hiCondExp))) {
         return accept(st"{ ${loCondExp.prettyST}; ${hiCondExp.prettyST} }", "is a subset of")
       } else {
         val sizeCond = hiCondExp.right