Fixed Inception inference on InvokeExp.

sireum · Oct 17, 2024 · 1780f3b · 1780f3b
1 parent 48a8665
commit 1780f3b
Showing 1 changed file with 6 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
@@ -165,6 +165,12 @@ object InceptionPlugin {
               ok = T
             case _ =>
           }
+          te match {
+            case te: AST.Exp.Invoke =>
+              ok = T
+              recInvoke(fe, te)
+            case _ =>
+          }
         case (fe: AST.Exp.Invoke, te: AST.Exp.Invoke) => recInvoke(fe, te)
         case (_, _) => ok = F
       }