From bef69b595b17ac3cd9c7b060aad400d6b6f99da2 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Mon, 28 Feb 2022 18:56:20 +0100
Subject: [PATCH] Ignore cex in SMT test

---
 .../smtCheckerTests/userTypes/multisource_module.sol         | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/test/libsolidity/smtCheckerTests/userTypes/multisource_module.sol b/test/libsolidity/smtCheckerTests/userTypes/multisource_module.sol
index 491b8600d..846f3ab75 100644
--- a/test/libsolidity/smtCheckerTests/userTypes/multisource_module.sol
+++ b/test/libsolidity/smtCheckerTests/userTypes/multisource_module.sol
@@ -16,6 +16,7 @@ contract C {
 // ====
 // SMTEngine: all
 // SMTIgnoreOS: macos
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (s2.sol:259-292): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h()\n    C.f(5) -- internal call\n    C.f(5) -- internal call
-// Warning 6328: (s2.sol:346-377): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h()\n    C.f(5) -- internal call\n    C.f(5) -- internal call\n    C.g(1) -- internal call\n    C.g(1) -- internal call
+// Warning 6328: (s2.sol:259-292): CHC: Assertion violation happens here.
+// Warning 6328: (s2.sol:346-377): CHC: Assertion violation happens here.