diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
index d72da3efa..cd6e1ef9b 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
@@ -11,6 +11,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // SMTIgnoreOS: macos
 // ----
 // Warning 4984: (82-85): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
diff --git a/test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol b/test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol
index ced7e37c4..699d22097 100644
--- a/test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol
+++ b/test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol
@@ -18,6 +18,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (407-457): CHC: Assertion violation happens here.
 // Info 1180: Contract invariant(s) for :C:\n(true || true || true)\nReentrancy property(ies) for :C:\n(((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(1))) == 1)\n<errorCode> = 2 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(2))) == 2)\n<errorCode> = 3 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 0xff)\n<errorCode> = 4 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 1)\n