From deb66c883e72a9c33a1435a4c36b0ca6a7eae2f4 Mon Sep 17 00:00:00 2001
From: zoep <zoe.paraskevopoulou@gmail.com>
Date: Wed, 4 Sep 2024 23:30:39 +0300
Subject: [PATCH] Support contract equality

---
 src/Act/HEVM.hs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Act/HEVM.hs b/src/Act/HEVM.hs
index bf0e7251..0a879633 100644
--- a/src/Act/HEVM.hs
+++ b/src/Act/HEVM.hs
@@ -445,6 +445,7 @@ toProp cmap = \case
   (LitBool _ b) -> pure $ EVM.PBool b
   (Eq _ SInteger e1 e2) -> op2 EVM.PEq e1 e2
   (Eq _ SBoolean e1 e2) -> op2 EVM.PEq e1 e2
+  (Eq _ SContract e1 e2) -> op2 EVM.PEq e1 e2
   (Eq _ _ _ _) -> error "unsupported"
   (NEq _ SInteger e1 e2) -> do
     e <- op2 EVM.PEq e1 e2
@@ -452,6 +453,9 @@ toProp cmap = \case
   (NEq _ SBoolean e1 e2) -> do
     e <- op2 EVM.PEq e1 e2
     pure $ EVM.PNeg e
+  (NEq _ SContract e1 e2) -> do
+    e <- op2 EVM.PEq e1 e2
+    pure $ EVM.PNeg e
   (NEq _ _ _ _) -> error "unsupported"
   (ITE _ _ _ _) -> error "Internal error: expecting flat expression"
   (Var _ _ _ _) -> error "TODO"
@@ -798,7 +802,6 @@ checkAliasing solver constructor@(Constructor _ (Interface ifaceName decls) prec
     prelude =  SMT2 src mempty mempty mempty
       where
         src = [ "; logic",
-                "; this is a test",
                 "(set-info :smt-lib-version 2.6)",
                 "(set-logic ALL)" ]