kore-rpc-client: ignore model when comparing GetModel results

runtimeverification · Aug 19, 2024 · 63b1c51 · 63b1c51
1 parent a667a9e
commit 63b1c51
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/booster/library/Booster/JsonRpc/Utils.hs b/booster/library/Booster/JsonRpc/Utils.hs
@@ -52,6 +52,10 @@ diffJson file1 file2 =
         -- useful when comparing responses of `kore-rpc` and `kore-rpc-booster`
         (contents1@(RpcResponse (Execute res1)), RpcResponse (Execute res2))
             | sameModuloBranchOrder res1 res2 -> Identical $ rpcTypeOf contents1
+        -- special case for GetModel results: only compare the satisfiable fields,
+        -- ignore variable assignments if present
+        (contents1@(RpcResponse (GetModel res1)), RpcResponse (GetModel res2))
+            | sameModuloModel res1 res2 -> Identical $ rpcTypeOf contents1
         (contents1, contents2)
             | contents1 == contents2 ->
                 Identical $ rpcTypeOf contents1
@@ -78,6 +82,9 @@ diffJson file1 file2 =
                 _ -> False
         | otherwise = False
 
+    sameModuloModel :: GetModelResult -> GetModelResult -> Bool
+    sameModuloModel res1 res2 = res1.satisfiable == res2.satisfiable
+
 data DiffResult
     = Identical KoreRpcType
     | DifferentType KoreRpcType KoreRpcType