Add get-model and simplify tests that Z3 cannot decide (#3737)

* add an integration test for when Z3 returns `unknown` during
`get-model`
* add an integration test for when Z3 returns `unknown` during
`simplify`
* add example error response into the docs

docs/2022-07-18-JSON-RPC-Server-API.md

@@ -734,6 +734,22 @@ This error wraps an error message from the internal implication check routine, i
 
 Error returned when the SMT solver crashes or is unable to discharge a goal.
 
+```json
+{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "error": {
+    "code": 5,
+    "message": "Smt solver error",
+    "data": {
+      "format": "KORE",
+      "version": 1,
+      "term": {}
+    }
+  }
+}
+```
+
 ## 6 Aborted
 
 ## 7 Multiple states

test/rpc-server/get-model/unknown/README.md

@@ -0,0 +1,4 @@
+# `get-model` applied to a predicate involving non-linear arithmetic
+
+* Input kore term: ` A == B ^ 256`
+* Result: `unknown`

test/rpc-server/get-model/unknown/definition.kore

@@ -0,0 +1 @@
+../../resources/int-and-bool/definition.kore

test/rpc-server/get-model/unknown/response.golden

@@ -0,0 +1 @@
+{"jsonrpc":"2.0","id":1,"result":{"satisfiable":"Unknown"}}

test/rpc-server/get-model/unknown/state.json

@@ -0,0 +1,67 @@
+{
+  "format": "KORE",
+  "version": 1,
+  "term": {
+    "tag": "Equals",
+    "argSort": {
+      "tag": "SortApp",
+      "name": "SortBool",
+      "args": []
+    },
+    "sort": {
+      "tag": "SortApp",
+      "name": "SortBool",
+      "args": []
+    },
+    "first": {
+      "tag": "DV",
+      "sort": {
+        "tag": "SortApp",
+        "name": "SortBool",
+        "args": []
+      },
+      "value": "true"
+    },
+    "second": {
+      "tag": "App",
+      "name": "Lbl'UndsEqlsEqls'Int'Unds'",
+      "sorts": [],
+      "args": [
+        {
+          "tag": "EVar",
+          "name": "X",
+          "sort": {
+            "tag": "SortApp",
+            "name": "SortInt",
+            "args": []
+          }
+        },
+        {
+          "tag": "App",
+          "name": "Lbl'UndsXor-'Int'Unds'",
+          "sorts": [],
+          "args": [
+            {
+              "tag": "EVar",
+              "name": "X",
+              "sort": {
+                "tag": "SortApp",
+                "name": "SortInt",
+                "args": []
+              }
+            },
+            {
+              "tag": "DV",
+              "sort": {
+                "tag": "SortApp",
+                "name": "SortInt",
+                "args": []
+              },
+              "value": "256"
+            }
+          ]
+        }
+      ]
+    }
+  }
+}

test/rpc-server/simplify/smt-error/README.md

@@ -0,0 +1,4 @@
+# Simplification of a predicate with a non-linear arithmetic sub-term
+
+* Input kore term: ` A == B ^ 256`
+* Result: Error response with code 5 and message "Smt solver error". Includes the patterns which the solver could not decide.

test/rpc-server/simplify/smt-error/definition.kore

@@ -0,0 +1 @@
+../../resources/int-and-bool/definition.kore

test/rpc-server/simplify/smt-error/response.golden

@@ -0,0 +1 @@
+{"jsonrpc":"2.0","id":1,"error":{"code":5,"data":{"format":"KORE","version":1,"term":{"tag":"And","sort":{"tag":"SortApp","name":"SortBool","args":[]},"patterns":[{"tag":"Ceil","argSort":{"tag":"SortApp","name":"SortInt","args":[]},"sort":{"tag":"SortApp","name":"SortBool","args":[]},"arg":{"tag":"App","name":"Lbl'UndsXor-'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"256"}]}},{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortInt","args":[]},"sort":{"tag":"SortApp","name":"SortBool","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortInt","args":[]}},"second":{"tag":"App","name":"Lbl'UndsXor-'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"256"}]}}]}},"message":"Smt solver error"}}

test/rpc-server/simplify/smt-error/state.json

@@ -0,0 +1,67 @@
+{
+  "format": "KORE",
+  "version": 1,
+  "term": {
+    "tag": "Equals",
+    "argSort": {
+      "tag": "SortApp",
+      "name": "SortBool",
+      "args": []
+    },
+    "sort": {
+      "tag": "SortApp",
+      "name": "SortBool",
+      "args": []
+    },
+    "first": {
+      "tag": "DV",
+      "sort": {
+        "tag": "SortApp",
+        "name": "SortBool",
+        "args": []
+      },
+      "value": "true"
+    },
+    "second": {
+      "tag": "App",
+      "name": "Lbl'UndsEqlsEqls'Int'Unds'",
+      "sorts": [],
+      "args": [
+        {
+          "tag": "EVar",
+          "name": "X",
+          "sort": {
+            "tag": "SortApp",
+            "name": "SortInt",
+            "args": []
+          }
+        },
+        {
+          "tag": "App",
+          "name": "Lbl'UndsXor-'Int'Unds'",
+          "sorts": [],
+          "args": [
+            {
+              "tag": "EVar",
+              "name": "X",
+              "sort": {
+                "tag": "SortApp",
+                "name": "SortInt",
+                "args": []
+              }
+            },
+            {
+              "tag": "DV",
+              "sort": {
+                "tag": "SortApp",
+                "name": "SortInt",
+                "args": []
+              },
+              "value": "256"
+            }
+          ]
+        }
+      ]
+    }
+  }
+}