Add test for the original issue

runtimeverification · May 24, 2022 · 2e7e1f3 · 2e7e1f3
1 parent ad5f101
commit 2e7e1f3
Show file tree

Hide file tree

Showing 3 changed files with 70 additions and 2 deletions.
diff --git a/k-distribution/tests/regression-new/json-input/json-in.k b/k-distribution/tests/regression-new/json-input/json-in.k
@@ -1,15 +1,15 @@
 // Copyright (c) 2019 K Team. All Rights Reserved.
 
 module JSON-IN-SYNTAX
-  imports INT-SYNTAX
+  imports INT
   imports ML-SYNTAX
 
   syntax Pgm ::= init ( Int )
   rule init(0) => { 3 #Equals 4 } [macro]
   rule init(1) => { 3 #Equals 3 } [macro]
+  configuration <k> $PGM:Pgm </k>
 endmodule
 
 module JSON-IN
   imports JSON-IN-SYNTAX
-  configuration <k color="green"> $PGM:Pgm </k>
 endmodule
diff --git a/k-distribution/tests/regression-new/json-input/json-in3.json.kast b/k-distribution/tests/regression-new/json-input/json-in3.json.kast
@@ -0,0 +1,63 @@
+{
+  "format": "KAST",
+  "version": 2,
+  "term": {
+    "node": "KApply",
+    "label": {
+      "node": "KLabel",
+      "name": "#And",
+      "params": [
+        {
+          "node": "KSort",
+          "name": "K"
+        }
+      ]
+    },
+    "variable": false,
+    "arity": 2,
+    "args": [
+      {
+        "node": "KApply",
+        "label": {
+          "node": "KLabel",
+          "name": "<k>",
+          "params": []
+        },
+        "variable": false,
+        "arity": 1,
+        "args": [
+          {
+            "node": "KVariable",
+            "name": "N",
+            "originalName": "N"
+          }
+        ]
+      },
+      {
+        "node": "KApply",
+        "label": {
+          "node": "KLabel",
+          "name": "_>=Int_",
+          "params": []
+        },
+        "variable": false,
+        "arity": 2,
+        "args": [
+          {
+            "node": "KVariable",
+            "name": "N",
+            "originalName": "N"
+          },
+          {
+            "node": "KToken",
+            "sort": {
+              "node": "KSort",
+              "name": "Int"
+            },
+            "token": "0"
+          }
+        ]
+      }
+    ]
+  }
+}
diff --git a/k-distribution/tests/regression-new/json-input/json-in3.json.kast.out b/k-distribution/tests/regression-new/json-input/json-in3.json.kast.out
@@ -0,0 +1,5 @@
+  <k>
+    N
+  </k>
+#And
+  N >=Int 0