From 7f06d6be43d087b97dc9e6ebc31f284755117d41 Mon Sep 17 00:00:00 2001
From: William E Bodell III <ratzbodell@gmail.com>
Date: Sun, 20 Nov 2022 16:36:10 -0600
Subject: [PATCH 1/3] Create smartian_motiv.sol

Add echidna-fied version of Smartian motivating example.
Original: https://github.com/SoftSec-KAIST/Smartian/blob/main/examples/sol/motiv.sol
---
 tests/solidity/research/smartian_motiv.sol | 36 ++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 tests/solidity/research/smartian_motiv.sol

diff --git a/tests/solidity/research/smartian_motiv.sol b/tests/solidity/research/smartian_motiv.sol
new file mode 100644
index 000000000..520095989
--- /dev/null
+++ b/tests/solidity/research/smartian_motiv.sol
@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+contract C {
+  address owner;
+  uint private stateA = 0;
+  uint private stateB = 0;
+  uint constant CONST = 32;
+  bool bug = false;
+
+  constructor() { // Constructor
+    owner = msg.sender;
+  }
+
+  function f(uint x) public {
+    if (msg.sender == owner) { 
+      stateA = x; 
+    }
+  }
+
+  function g(uint y) public {
+    if (stateA % CONST == 1) {
+      stateB = y - 10;
+    }
+  }
+
+  function h() public {
+    if (stateB == 62) { 
+      bug = true; 
+    }
+  }
+
+  function echidna_bug() public returns (bool) {
+    return !bug;
+  }
+}

From f07de4b2f866f9a46d72b2a0b8abc8e51a9cc28b Mon Sep 17 00:00:00 2001
From: William E Bodell III <ratzbodell@gmail.com>
Date: Sun, 20 Nov 2022 16:39:53 -0600
Subject: [PATCH 2/3] Create smartian_motiv.yaml

Add config file for Smartian motivating example
---
 tests/solidity/research/smartian_motiv.yaml | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 tests/solidity/research/smartian_motiv.yaml

diff --git a/tests/solidity/research/smartian_motiv.yaml b/tests/solidity/research/smartian_motiv.yaml
new file mode 100644
index 000000000..f28ffc972
--- /dev/null
+++ b/tests/solidity/research/smartian_motiv.yaml
@@ -0,0 +1,3 @@
+seqLen: 10  
+deployer: "0x20000"
+sender: ["0x10000", "0x20000"]

From 0f0e5c42a65c244b5fc1af4b4cb8a659d8bd3f1e Mon Sep 17 00:00:00 2001
From: William E Bodell III <ratzbodell@gmail.com>
Date: Sun, 20 Nov 2022 16:53:02 -0600
Subject: [PATCH 3/3] Update smartian_motiv.yaml

Set a higher testLimit, since the default 50,000 isn't cutting it
---
 tests/solidity/research/smartian_motiv.yaml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tests/solidity/research/smartian_motiv.yaml b/tests/solidity/research/smartian_motiv.yaml
index f28ffc972..570a30206 100644
--- a/tests/solidity/research/smartian_motiv.yaml
+++ b/tests/solidity/research/smartian_motiv.yaml
@@ -1,3 +1,4 @@
+testLimit: 999999
 seqLen: 10  
 deployer: "0x20000"
 sender: ["0x10000", "0x20000"]