From 16535aae3272e676a140ea94e3f2a757a2ee20ec Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Wed, 1 Dec 2021 17:38:23 +0100
Subject: [PATCH] Fix ICE when unsafe targets are solved more than once and the
 cex is different

---
 Changelog.md                                  |  1 +
 libsolidity/formal/CHC.cpp                    |  2 -
 .../smtCheckerTests/imports/ExtCall.sol       | 42 +++++++++++++++++++
 3 files changed, 43 insertions(+), 2 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/imports/ExtCall.sol

diff --git a/Changelog.md b/Changelog.md
index b3af54d04..e24cb2462 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -8,6 +8,7 @@ Compiler Features:
 
 Bugfixes:
  * Code Generator: Fix a crash when using ``@use-src`` and compiling from Yul to ewasm.
+ * SMTChecker: Fix internal error when an unsafe target is solved more than once and the counterexample messages are different.
 
 
 ### 0.8.10 (2021-11-09)
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 76a5ded99..0edfc27ff 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -972,8 +972,6 @@ void CHC::resetSourceAnalysis()
 {
 	SMTEncoder::resetSourceAnalysis();
 
-	m_safeTargets.clear();
-	m_unsafeTargets.clear();
 	m_unprovedTargets.clear();
 	m_invariants.clear();
 	m_functionTargetIds.clear();
diff --git a/test/libsolidity/smtCheckerTests/imports/ExtCall.sol b/test/libsolidity/smtCheckerTests/imports/ExtCall.sol
new file mode 100644
index 000000000..047148a90
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/imports/ExtCall.sol
@@ -0,0 +1,42 @@
+==== Source: ExtCall.sol ====
+interface Unknown {
+    function callme() external;
+}
+
+contract ExtCall {
+    uint x;
+
+    bool lock;
+    modifier mutex {
+        require(!lock);
+        lock = true;
+        _;
+        lock = false;
+    }
+
+    function setX(uint y) mutex public {
+        x = y;
+    }
+
+    function xMut(Unknown u) public {
+        uint x_prev = x;
+        u.callme();
+        assert(x_prev == x);
+    }
+}
+==== Source: ExtCall.t.sol ====
+import "ExtCall.sol";
+
+contract ExtCallTest {
+    ExtCall call;
+
+    function setUp() public {
+        call = new ExtCall();
+    }
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (ExtCall.sol:362-381): CHC: Assertion violation happens here.
+// Warning 4588: (ExtCall.t.sol:110-123): Assertion checker does not yet implement this type of function call.