From 0660842dc4e73c2758a8e05fbd8101519c0d2916 Mon Sep 17 00:00:00 2001
From: David Terry <me@xwvvvvwx.com>
Date: Mon, 20 Jun 2022 15:39:31 +0200
Subject: [PATCH 1/4] dapp: readme: fixup tutorial

---
 src/dapp/README.md | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/dapp/README.md b/src/dapp/README.md
index e6be69404..227edc135 100644
--- a/src/dapp/README.md
+++ b/src/dapp/README.md
@@ -50,6 +50,7 @@ Let's create a new `dapp` project. We make a new directory and initialize the `d
 
 ```sh
 mkdir dapptutorial
+cd dapptutorial
 dapp init
 ```
 
@@ -87,6 +88,9 @@ Compile the contract by running `dapp build`. If you didn't make any mistakes, y
 Let's write some tests for our vault. Change `Dapptutorial.t.sol` to the following. We'll go over whats going on in the next paragraph.
 
 ```solidity
+import {DSTest} from "ds-test/test.sol";
+import {Dapptutorial} from "./Dapptutorial.sol";
+
 contract DapptutorialTest is DSTest {
     Dapptutorial dapptutorial;
 
@@ -110,8 +114,7 @@ contract DapptutorialTest is DSTest {
         assertEq(preBalance + 1 ether, postBalance);
     }
 
-    receive() external payable {
-    }
+    receive() external payable {}
 }
 ```
 

From 75e02498651aaec59397187fa1555a97db7d6d69 Mon Sep 17 00:00:00 2001
From: David Terry <me@xwvvvvwx.com>
Date: Mon, 20 Jun 2022 15:51:17 +0200
Subject: [PATCH 2/4] hevm: unit tests: handle concrete returndata for symbolic
 tests

---
 src/hevm/src/EVM/UnitTest.hs | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/hevm/src/EVM/UnitTest.hs b/src/hevm/src/EVM/UnitTest.hs
index ca23b2db4..a60626f70 100644
--- a/src/hevm/src/EVM/UnitTest.hs
+++ b/src/hevm/src/EVM/UnitTest.hs
@@ -694,9 +694,11 @@ symRun opts@UnitTestOptions{..} concreteVm testName types = do
         SBV.resetAssertions
         constrain $ sAnd (fst <$> view EVM.constraints vm')
         unless bailed $
-          case view result vm' of
-            Just (VMSuccess (SymbolicBuffer buf)) ->
-              constrain $ litBytes (encodeAbiValue $ AbiBool $ not shouldFail) .== buf
+          let
+            checkResult buf = constrain $ litBytes (encodeAbiValue $ AbiBool $ not shouldFail) .== buf
+          in case view result vm' of
+            Just (VMSuccess (SymbolicBuffer buf)) -> checkResult buf
+            Just (VMSuccess (ConcreteBuffer buf)) -> checkResult (litBytes buf)
             r -> error $ "unexpected return value: " ++ show r
         checkSat >>= \case
           Sat -> do

From 94c2e0323cbcb50a9a82e8c25fd084fa031af3d8 Mon Sep 17 00:00:00 2001
From: David Terry <me@xwvvvvwx.com>
Date: Mon, 20 Jun 2022 15:51:46 +0200
Subject: [PATCH 3/4] hevm: tests: add testcase for symbolic test with concrete
 returndata

---
 src/dapp-tests/default.nix          |  1 +
 src/dapp-tests/fail/dsProveFail.sol | 23 +++++++++++++++++++++++
 src/dapp/README.md                  |  1 +
 3 files changed, 25 insertions(+)

diff --git a/src/dapp-tests/default.nix b/src/dapp-tests/default.nix
index b559c258d..8134d8e96 100644
--- a/src/dapp-tests/default.nix
+++ b/src/dapp-tests/default.nix
@@ -163,6 +163,7 @@ in
       invariant-first = fail "invariantFirst";
       invariant-test-usr-bal = fail "invariantTestUserBal";
       invariant-test-initial-inv-call = fail "invariantCount";
+      withdraw = fail "proveFail_withdraw";
     };
 
     dss = pkgs.buildDappPackage {
diff --git a/src/dapp-tests/fail/dsProveFail.sol b/src/dapp-tests/fail/dsProveFail.sol
index fedf07fcc..e59fd4782 100644
--- a/src/dapp-tests/fail/dsProveFail.sol
+++ b/src/dapp-tests/fail/dsProveFail.sol
@@ -4,11 +4,23 @@ import "ds-test/test.sol";
 import "ds-token/token.sol";
 import "ds-math/math.sol";
 
+contract Withdraw {
+    receive() external payable {}
+
+    function withdraw(uint password) public {
+        require(password == 42, "Access denied!");
+        payable(msg.sender).transfer(address(this).balance);
+    }
+}
+
+
 contract SolidityTest is DSTest, DSMath {
     DSToken token;
+    Withdraw withdraw;
 
     function setUp() public {
         token = new DSToken("TKN");
+        withdraw = new Withdraw();
     }
 
     function prove_add(uint x, uint y) public {
@@ -59,5 +71,16 @@ contract SolidityTest is DSTest, DSMath {
                         : amt; // otherwise `amt` has been transfered to `usr`
         assertEq(expected, postbal - prebal);
     }
+
+    function proveFail_withdraw(uint guess) public {
+        payable(address(withdraw)).transfer(1 ether);
+        uint preBalance = address(this).balance;
+        withdraw.withdraw(guess);
+        uint postBalance = address(this).balance;
+        assertEq(preBalance + 1 ether, postBalance);
+    }
+
+    // allow sending eth to the test contract
+    receive() external payable {}
 }
 
diff --git a/src/dapp/README.md b/src/dapp/README.md
index 227edc135..a7773fb62 100644
--- a/src/dapp/README.md
+++ b/src/dapp/README.md
@@ -114,6 +114,7 @@ contract DapptutorialTest is DSTest {
         assertEq(preBalance + 1 ether, postBalance);
     }
 
+    // allow sending eth to the test contract
     receive() external payable {}
 }
 ```

From 36dc24a5966e195c1c0b677bec57eca375f7c554 Mon Sep 17 00:00:00 2001
From: David Terry <me@xwvvvvwx.com>
Date: Mon, 20 Jun 2022 16:00:10 +0200
Subject: [PATCH 4/4] hevm: changelog: update

---
 src/hevm/CHANGELOG.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/hevm/CHANGELOG.md b/src/hevm/CHANGELOG.md
index 7de2be982..3e1dcc660 100644
--- a/src/hevm/CHANGELOG.md
+++ b/src/hevm/CHANGELOG.md
@@ -12,6 +12,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Support for solc 0.8.12
 - Support for solc 0.8.13
 
+### Fixed
+
+- Correctly handle concrete returndata when checking the result of a symbolic test
+
 ## [0.49.0] - 2021-11-12
 
 ### Added