From 923b012251ec0f77757d0ec06ec68440dab066d2 Mon Sep 17 00:00:00 2001
From: Robby <robby@santoslab.org>
Date: Tue, 19 Mar 2024 13:30:10 -0500
Subject: [PATCH] Fixed implication symbols.

---
 shared/src/main/scala/org/sireum/logika/Logika.scala | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala
index c782e2bc..670f3b40 100644
--- 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