add another test

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") ]
   ]

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
+        }
+    }
+}

tests/solidity/symbolic/sym-assert.yaml

@@ -0,0 +1,3 @@
+testMode: assertion
+symExec: true
+workers: 0

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);
+    }
 }

tests/solidity/symbolic/sym.yaml

@@ -1,3 +1,2 @@
-testMode: assertion
 symExec: true
 workers: 0