Added inception inference on Z and B literals.

sireum · Sep 12, 2023 · f655a9a · f655a9a
1 parent ba1b6dc
commit f655a9a
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala
@@ -85,6 +85,10 @@ object InceptionPlugin {
         return
       }
       (fe, te) match {
+        case (fe: AST.Exp.LitB, te: AST.Exp.LitB) =>
+          ok = fe.value == te.value
+        case (fe: AST.Exp.LitZ, te: AST.Exp.LitZ) =>
+          ok = fe.value == te.value
         case (fe: AST.Exp.Ident, te) =>
           if (shouldExtract(fe.resOpt)) {
             addResult(fe.id.value, te)
@@ -314,6 +318,9 @@ import InceptionPlugin._
         return emptyResult
       }
       val id = name(name.size - 1)
+      if (id == "AllE") {
+        println("Here")
+      }
       var ok = T
       var idExpMap = HashSMap.empty[String, AST.Exp]
       val paramIds = HashSet ++ paramNames