Restrict the scope of bool pred internalisation to syntactic transfor…

…mation only (#3945) Fixes #3938
runtimeverification · Jun 18, 2024 · 974ab83 · 974ab83
1 parent e845c00
commit 974ab83
Show file tree

Hide file tree

Showing 3 changed files with 349 additions and 286 deletions.
diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs
@@ -429,27 +429,20 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort
     Syntax.KJBottom{} -> notSupported
     Syntax.KJNot{arg} -> do
         recursion arg >>= \case
-            [BoolPred (Internal.Predicate (Internal.EqualsInt a b))] ->
-                pure [BoolPred $ Internal.Predicate $ Internal.NEqualsInt a b]
-            [BoolPred (Internal.Predicate (Internal.NEqualsInt a b))] ->
-                pure [BoolPred $ Internal.Predicate $ Internal.EqualsInt a b]
-            [BoolPred (Internal.Predicate (Internal.EqualsK a b))] ->
-                pure [BoolPred $ Internal.Predicate $ Internal.NEqualsK a b]
-            [BoolPred (Internal.Predicate (Internal.NEqualsK a b))] ->
-                pure [BoolPred $ Internal.Predicate $ Internal.EqualsK a b]
             [BoolPred (Internal.Predicate p')] ->
                 pure [BoolPred $ Internal.Predicate $ Internal.NotBool p']
             [SubstitutionPred k v] ->
                 if "@" `isPrefixOf` k.variableName
                     then notSupported -- @ variables are set variables, the negation of which we do not support internalising
                     else case sortOfTerm v of
                         Internal.SortInt ->
-                            pure [BoolPred $ Internal.Predicate $ Internal.NEqualsInt (Internal.Var k) v]
+                            pure [BoolPred $ Internal.Predicate $ Internal.NotBool $ Internal.EqualsInt (Internal.Var k) v]
                         otherSort ->
                             pure
                                 [ BoolPred $
                                     Internal.Predicate $
-                                        Internal.NEqualsK (Internal.KSeq otherSort $ Internal.Var k) (Internal.KSeq otherSort v)
+                                        Internal.NotBool $
+                                            Internal.EqualsK (Internal.KSeq otherSort $ Internal.Var k) (Internal.KSeq otherSort v)
                                 ]
             _ -> notSupported
     Syntax.KJAnd{patterns = []} -> notSupported