Add integration test with non-linear constraint

Author: geo2a

booster/test/rpc-integration/resources/non-linear-int-requires/test.k

@@ -0,0 +1,17 @@
+module TEST
+  imports INT
+  imports BOOL
+
+  syntax State ::= "init"   [token]
+                 | "target" [token]
+
+  configuration <k> $PGM:State ~> .K </k>
+                <x-int> 0:Int          </x-int>
+                <y-int> 0:Int          </y-int>
+
+  rule [transition]: <k> init => target ... </k>
+                     <x-int> X              </x-int>
+                     <y-int> Y              </y-int>
+       requires X <Int (X *Int Y +Int Y) /Int (Y /Int X)
+
+endmodule

booster/test/rpc-integration/test-non-linear-int-requires/README.md

@@ -0,0 +1 @@
+This test is useful for debugging the SMT solver retry logic. To force the solver to return unknown and retry, run the server with a very short SMT timeout, e.g. `booster-dev --smt-timeout 1`.

booster/test/rpc-integration/test-non-linear-int-requires/response-init.json

@@ -0,0 +1,2 @@
+{"jsonrpc":"2.0","id":1,"result":{"reason":"aborted","depth":0,"state":{"term":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'-LT-'generatedTop'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'k'-GT-'","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortState","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortState","args":[]},"value":"init"}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}]},{"tag":"App","name":"Lbl'-LT-'x-int'-GT-'","sorts":[],"args":[{"tag":"EVar","name":"VarX","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]},{"tag":"App","name":"Lbl'-LT-'y-int'-GT-'","sorts":[],"args":[{"tag":"EVar","name":"VarY","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]},{"tag":"App","name":"Lbl'-LT-'generatedCounter'-GT-'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]}}}}}
+

booster/test/rpc-integration/test-non-linear-int-requires/state-init.execute

@@ -0,0 +1,90 @@
+{
+  "format": "KORE",
+  "version": 1,
+  "term": {
+    "tag": "App",
+    "name": "Lbl'-LT-'generatedTop'-GT-'",
+    "sorts": [],
+    "args": [
+      {
+        "tag": "App",
+        "name": "Lbl'-LT-'k'-GT-'",
+        "sorts": [],
+        "args": [
+          {
+            "tag": "App",
+            "name": "kseq",
+            "sorts": [],
+            "args": [
+              {
+                "tag": "App",
+                "name": "inj",
+                "sorts": [
+                  {
+                    "tag": "SortApp",
+                    "name": "SortState",
+                    "args": []
+                  },
+                  {
+                    "tag": "SortApp",
+                    "name": "SortKItem",
+                    "args": []
+                  }
+                ],
+                "args": [
+                  {
+                    "tag": "DV",
+                    "sort": {
+                      "tag": "SortApp",
+                      "name": "SortState",
+                      "args": []
+                    },
+                    "value": "init"
+                  }
+                ]
+              },
+              {
+                "tag": "App",
+                "name": "dotk",
+                "sorts": [],
+                "args": []
+              }
+            ]
+          }
+        ]
+      },
+      {
+        "tag": "App",
+        "name": "Lbl'-LT-'x-int'-GT-'",
+        "sorts": [],
+        "args": [
+          {"tag":"EVar","name":"VarX","sort":{"tag":"SortApp","name":"SortInt","args":[]}}
+        ]
+      },
+      {
+        "tag": "App",
+        "name": "Lbl'-LT-'y-int'-GT-'",
+        "sorts": [],
+        "args": [
+          {"tag":"EVar","name":"VarY","sort":{"tag":"SortApp","name":"SortInt","args":[]}}
+        ]
+      },
+      {
+        "tag": "App",
+        "name": "Lbl'-LT-'generatedCounter'-GT-'",
+        "sorts": [],
+        "args": [
+          {
+            "tag": "DV",
+            "sort": {
+              "tag": "SortApp",
+              "name": "SortInt",
+              "args": []
+            },
+            "value": "0"
+          }
+        ]
+      }
+    ]
+  }
+}