Use 8-bit encoding for external syntax of BYTES.Bytes

Author: ttuegel

kore/src/Kore/Builtin/InternalBytes.hs

@@ -149,7 +149,7 @@ patternVerifierHook =
     patternVerifierWorker external =
         case externalChild of
             StringLiteral_ literal -> do
-                bytesValue <- Builtin.parseString Encoding.parseBase16 literal
+                bytesValue <- Builtin.parseString Encoding.parse8Bit literal
                 (return . InternalBytesF . Const)
                     InternalBytes { bytesSort, bytesValue }
             _ -> Kore.Error.koreFail "Expected literal string"

kore/src/Kore/Builtin/InternalBytes/InternalBytes.hs

@@ -96,7 +96,7 @@ asTermLike
 asTermLike InternalBytes { bytesSort, bytesValue }  =
     mkDomainValue DomainValue
         { domainValueSort = bytesSort
-        , domainValueChild = mkStringLiteral $ Encoding.toBase16 bytesValue
+        , domainValueChild = mkStringLiteral $ Encoding.decode8Bit bytesValue
         }
 
 internalize

kore/test/Test/Kore/Builtin/InternalBytes.hs

@@ -603,6 +603,14 @@ test_InternalBytes =
                 mkDomainValue
                 $ DomainValue bytesSort
                 $ mkStringLiteral "00"
+            expect = Right $ asInternal "00"
+            actual = verifyPattern (Just bytesSort) unverified
+        assertEqual "" expect actual
+    , testCase "\\dv{Bytes{}}(\"\x00\")" $ do
+        let unverified =
+                mkDomainValue
+                $ DomainValue bytesSort
+                $ mkStringLiteral "\x00"
             expect = Right $ asInternal "\x00"
             actual = verifyPattern (Just bytesSort) unverified
         assertEqual "" expect actual