From 795226d4f9dfc5b3bbc8c4f3d5c587f33cabeb46 Mon Sep 17 00:00:00 2001
From: Sam Alws <sam.alws@trailofbits.com>
Date: Wed, 10 Apr 2024 12:19:52 -0400
Subject: [PATCH] add another test

---
 src/test/Tests/Symbolic.hs              |  8 +++++---
 tests/solidity/symbolic/sym-assert.sol  | 15 +++++++++++++++
 tests/solidity/symbolic/sym-assert.yaml |  3 +++
 tests/solidity/symbolic/sym.sol         | 10 ++++++++--
 tests/solidity/symbolic/sym.yaml        |  1 -
 5 files changed, 31 insertions(+), 6 deletions(-)
 create mode 100644 tests/solidity/symbolic/sym-assert.sol
 create mode 100644 tests/solidity/symbolic/sym-assert.yaml

diff --git a/src/test/Tests/Symbolic.hs b/src/test/Tests/Symbolic.hs
index 5219c30e9..f3d33fc05 100644
--- a/src/test/Tests/Symbolic.hs
+++ b/src/test/Tests/Symbolic.hs
@@ -2,13 +2,15 @@ module Tests.Symbolic (symbolicTests) where
 
 import System.Info (os)
 import Test.Tasty (TestTree, testGroup)
-import Common (testContract', solved)
+import Common (testContract', solved, passed)
 import Echidna.Types.Campaign (WorkerType(..))
 
 symbolicTests :: TestTree
 symbolicTests = testGroup "Symbolic tests" $ if os /= "linux" then [] else
-  [
-    testContract' "symbolic/sym.sol" Nothing Nothing (Just "symbolic/sym.yaml") True SymbolicWorker
+  [ testContract' "symbolic/sym.sol" Nothing Nothing (Just "symbolic/sym.yaml") True SymbolicWorker
+      [ ("echidna_sym passed", passed "echidna_sym") ]
+
+  , testContract' "symbolic/sym-assert.sol" Nothing Nothing (Just "symbolic/sym-assert.yaml") True SymbolicWorker
       [ ("func_one passed", solved "func_one")
       , ("func_two passed", solved "func_two") ]
   ]
diff --git a/tests/solidity/symbolic/sym-assert.sol b/tests/solidity/symbolic/sym-assert.sol
new file mode 100644
index 000000000..7b994d2a4
--- /dev/null
+++ b/tests/solidity/symbolic/sym-assert.sol
@@ -0,0 +1,15 @@
+contract VulnerableContract {
+    mapping (uint256 => uint256) a;
+    function func_one(uint256 x) public payable {
+        a[12323] = ((x >> 5) / 7777);
+        if (a[12323] == 2222) {
+            assert(false); // BUG
+        }
+    }
+
+    function func_two(uint256 x) public payable {
+        if ((x >> 5) / 7777 == 2222) {
+            assert(false); // BUG
+        }
+    }
+}
diff --git a/tests/solidity/symbolic/sym-assert.yaml b/tests/solidity/symbolic/sym-assert.yaml
new file mode 100644
index 000000000..8fe6b7432
--- /dev/null
+++ b/tests/solidity/symbolic/sym-assert.yaml
@@ -0,0 +1,3 @@
+testMode: assertion
+symExec: true
+workers: 0
diff --git a/tests/solidity/symbolic/sym.sol b/tests/solidity/symbolic/sym.sol
index 7b994d2a4..8b46a52a7 100644
--- a/tests/solidity/symbolic/sym.sol
+++ b/tests/solidity/symbolic/sym.sol
@@ -1,15 +1,21 @@
 contract VulnerableContract {
     mapping (uint256 => uint256) a;
+    bool y;
+    bool z;
     function func_one(uint256 x) public payable {
         a[12323] = ((x >> 5) / 7777);
         if (a[12323] == 2222) {
-            assert(false); // BUG
+            y = true;
         }
     }
 
     function func_two(uint256 x) public payable {
         if ((x >> 5) / 7777 == 2222) {
-            assert(false); // BUG
+            z = true;
         }
     }
+
+    function echidna_sym() public returns (bool) {
+        return !(y && z);
+    }
 }
diff --git a/tests/solidity/symbolic/sym.yaml b/tests/solidity/symbolic/sym.yaml
index 8fe6b7432..e152e2a1b 100644
--- a/tests/solidity/symbolic/sym.yaml
+++ b/tests/solidity/symbolic/sym.yaml
@@ -1,3 +1,2 @@
-testMode: assertion
 symExec: true
 workers: 0