From 63b1c513e2f1dab7b6590ac93558b9f10f6f51c7 Mon Sep 17 00:00:00 2001
From: Georgy Lukyanov <mail@geo2a.info>
Date: Mon, 19 Aug 2024 14:40:28 +0200
Subject: [PATCH] kore-rpc-client: ignore model when comparing GetModel results

---
 booster/library/Booster/JsonRpc/Utils.hs | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/booster/library/Booster/JsonRpc/Utils.hs b/booster/library/Booster/JsonRpc/Utils.hs
index 0e299f3dc2..f27e3e7909 100644
--- 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