From 5f1da8c59aa3232b11d607368de484b0501fdef3 Mon Sep 17 00:00:00 2001
From: Mark Spanbroek <mark@spanbroek.net>
Date: Wed, 25 Jan 2023 11:57:20 +0100
Subject: [PATCH] [build] Allow model checking with solidity compiler

---
 hardhat.modelcheck.config.js | 11 +++++++++++
 package.json                 |  3 ++-
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 hardhat.modelcheck.config.js

diff --git a/hardhat.modelcheck.config.js b/hardhat.modelcheck.config.js
new file mode 100644
index 0000000..09b7d0f
--- /dev/null
+++ b/hardhat.modelcheck.config.js
@@ -0,0 +1,11 @@
+const config = require("./hardhat.config")
+
+config.solidity.settings.modelChecker = {
+  engine: "chc",
+  showUnproved: true,
+  contracts: {
+    "contracts/TestCollateral.sol": ["TestCollateral"],
+  },
+}
+
+module.exports = config
diff --git a/package.json b/package.json
index 99abdfb..42a5b01 100644
--- a/package.json
+++ b/package.json
@@ -5,7 +5,8 @@
     "test": "npm run lint && hardhat test",
     "start": "hardhat node --export deployment-localhost.json",
     "format": "prettier --write contracts/**/*.sol test/**/*.js",
-    "lint": "solhint contracts/**.sol"
+    "lint": "solhint contracts/**.sol",
+    "modelcheck": "hardhat compile --config hardhat.modelcheck.config.js --force"
   },
   "devDependencies": {
     "@nomiclabs/hardhat-ethers": "^2.2.1",