Merge pull request #12358 from ethereum/smt_fix_targets

Fix ICE when unsafe targets are solved more than once and the cex is !=

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)

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();

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.