From 39232593cf7664e446f4557e600adb3012f16794 Mon Sep 17 00:00:00 2001
From: liav-certora <liav@certora.com>
Date: Tue, 5 Mar 2024 11:26:02 +0200
Subject: [PATCH] mutations fixes

---
 DEFI/ERC20/mutation.conf          | 22 ++++++++++++++++++++++
 DEFI/ERC20/mutation.mconf         | 11 -----------
 DEFI/LiquidityPool/mutation.conf  | 20 ++++++++++++++++++++
 DEFI/LiquidityPool/mutation.mconf |  6 ------
 4 files changed, 42 insertions(+), 17 deletions(-)
 create mode 100644 DEFI/ERC20/mutation.conf
 delete mode 100644 DEFI/ERC20/mutation.mconf
 create mode 100644 DEFI/LiquidityPool/mutation.conf
 delete mode 100644 DEFI/LiquidityPool/mutation.mconf

diff --git a/DEFI/ERC20/mutation.conf b/DEFI/ERC20/mutation.conf
new file mode 100644
index 00000000..86d9ed14
--- /dev/null
+++ b/DEFI/ERC20/mutation.conf
@@ -0,0 +1,22 @@
+{
+    "files": [
+      "contracts/ERC20.sol"
+    ],
+    "verify": "ERC20:certora/specs/ERC20Full.spec",
+    "msg": "ERC20 Full spec",
+    "rule_sanity": "basic",
+    "optimistic_loop": true,
+    "mutations": {
+        "gambit": {
+                  "filename" : "contracts/ERC20.sol",
+                  "num_mutants": 57
+        },
+        "manual_mutants": [
+            {
+              "file_to_mutate": "contracts/ERC20.sol", 
+              "mutants_location": "mutant"
+            }
+        ],
+        "msg": "ERC20 mutations"
+    }
+}
\ No newline at end of file
diff --git a/DEFI/ERC20/mutation.mconf b/DEFI/ERC20/mutation.mconf
deleted file mode 100644
index c8b7d6a4..00000000
--- a/DEFI/ERC20/mutation.mconf
+++ /dev/null
@@ -1,11 +0,0 @@
-{ 
-  "gambit": {
-            "filename" : "contracts/ERC20.sol",
-            "num_mutants": 57
-  },
-  
-  "manual_mutants": {
-     "contracts/ERC20.sol": "mutant"
-  },
-  "msg": "ERC20 mutations"
-}
\ No newline at end of file
diff --git a/DEFI/LiquidityPool/mutation.conf b/DEFI/LiquidityPool/mutation.conf
new file mode 100644
index 00000000..b3e4bce3
--- /dev/null
+++ b/DEFI/LiquidityPool/mutation.conf
@@ -0,0 +1,20 @@
+{
+  "files": [
+    "contracts/Pool.sol",
+    "contracts/Asset.sol",
+    "certora/harness/TrivialReceiver.sol"
+  ],
+  "verify": "Pool:certora/specs/Full.spec",
+  "msg": "Pool with linking",
+  "link": [
+        "Pool:asset=Asset"
+    ],
+  "parametric_contracts": ["Pool"],
+  "rule_sanity": "basic",
+  "mutations": {
+      "gambit": {
+        "filename" : "contracts/Pool.sol",
+        "num_mutants": 30
+      }
+  }
+}
\ No newline at end of file
diff --git a/DEFI/LiquidityPool/mutation.mconf b/DEFI/LiquidityPool/mutation.mconf
deleted file mode 100644
index a064d546..00000000
--- a/DEFI/LiquidityPool/mutation.mconf
+++ /dev/null
@@ -1,6 +0,0 @@
-{ 
-  "gambit": {
-            "filename" : "contracts/Pool.sol",
-            "num_mutants": 30
-  }
-}
\ No newline at end of file