Fixed implication symbols.

sireum · Mar 19, 2024 · 923b012 · 923b012
1 parent 042d4d7
commit 923b012
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala
@@ -633,7 +633,7 @@ object Logika {
             e.op match {
               case AST.Exp.BinaryOp.And =>
               case AST.Exp.BinaryOp.Or =>
-              case AST.Exp.BinaryOp.Imply =>
+              case "->:" =>
               case _ => hasError = T
             }
             checkExp(e.left)
@@ -743,8 +743,8 @@ object Logika {
               val r: B = e.op match {
                 case AST.Exp.BinaryOp.And => evalExp(e.left) & evalExp(e.right)
                 case AST.Exp.BinaryOp.Or => evalExp(e.left) | evalExp(e.right)
-                case AST.Exp.BinaryOp.Imply => !evalExp(e.left) | evalExp(e.right)
-                case _ => F
+                case "->:" => !evalExp(e.left) | evalExp(e.right)
+                case _ => halt(s"Infeasible: ${e.op}")
               }
               putResult(r, F)
               return r