diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d.sol index bbd5589a4..34b439e3a 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d.sol @@ -20,5 +20,6 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreCex: yes // ---- // Warning 6328: (362-420): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol index f9997c163..ddd4b41e6 100644 --- a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol @@ -18,6 +18,7 @@ contract C { // ==== // SMTEngine: all // SMTExtCalls: trusted +// SMTIgnoreOS: macos // ---- // Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 6328: (167-185): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol index cc54f3a09..5e81ffd1c 100644 --- a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol @@ -17,6 +17,7 @@ contract C { // ==== // SMTEngine: all // SMTExtCalls: trusted +// SMTIgnoreOS: macos // ---- // Warning 1218: (233-251): CHC: Error trying to invoke SMT solver. // Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol index c066778cb..7905d5b4f 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol @@ -21,7 +21,8 @@ contract C { // ==== // SMTEngine: chc // SMTExtCalls: trusted +// SMTIgnoreCex: yes // ---- -// Warning 6328: (231-253): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0119\ny = 0\n\nTransaction trace:\nC.constructor() -// Warning 6328: (293-307): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0217\ny = 3\n\nTransaction trace:\nC.constructor() -// Warning 6328: (359-374): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x188b\ny = 0\n\nTransaction trace:\nC.constructor() +// Warning 6328: (231-253): CHC: Assertion violation happens here. +// Warning 6328: (293-307): CHC: Assertion violation happens here. +// Warning 6328: (359-374): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol index af19ce898..25cccead4 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol @@ -17,8 +17,9 @@ contract C { // ==== // SMTEngine: chc // SMTExtCalls: trusted +// SMTIgnoreCex: yes // ---- // Warning 9302: (257-293): Return value of low-level calls not used. -// Warning 6328: (216-238): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0119\n\nTransaction trace:\nC.constructor() -// Warning 6328: (297-319): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x1720\n\nTransaction trace:\nC.constructor() -// Warning 6328: (404-426): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x1720\n\nTransaction trace:\nC.constructor() +// Warning 6328: (216-238): CHC: Assertion violation happens here. +// Warning 6328: (297-319): CHC: Assertion violation happens here. +// Warning 6328: (404-426): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol index 4fef1dc99..b7a161ac9 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol @@ -35,6 +35,7 @@ contract C { // ==== // SMTEngine: chc // SMTExtCalls: trusted +// SMTIgnoreOS: macos // ---- // Warning 6328: (256-277): CHC: Assertion violation happens here. // Warning 6328: (533-554): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol index 2928d20f3..60bfd1660 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol @@ -40,5 +40,6 @@ contract C { // ==== // SMTEngine: chc // SMTExtCalls: trusted +// SMTIgnoreOS: macos // ---- // Warning 6328: (561-582): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol index e115eb0e3..4e86c7b2b 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol @@ -43,5 +43,6 @@ contract C { // ==== // SMTEngine: chc // SMTExtCalls: trusted +// SMTIgnoreOS: macos // ---- // Warning 6328: (641-662): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol index 5e1ad8b1b..51c9cb734 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol @@ -12,5 +12,6 @@ contract C { // SMTEngine: chc // SMTExtCalls: trusted // SMTTargets: assert +// SMTIgnoreCex: yes // ---- -// Warning 6328: (147-161): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.i() -- trusted external call +// Warning 6328: (147-161): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_2.sol index 9c9682f81..baeddda08 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_2.sol @@ -16,5 +16,6 @@ contract C { // SMTEngine: chc // SMTExtCalls: trusted // SMTTargets: assert +// SMTIgnoreCex: yes // ---- -// Warning 6328: (165-187): CHC: Assertion violation happens here.\nCounterexample:\nds = [37]\n\nTransaction trace:\nC.constructor()\nState: ds = [37]\nC.f() +// Warning 6328: (165-187): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol index 19f39b1d9..4d179ddf8 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol @@ -38,6 +38,7 @@ contract C { // SMTContract: C // SMTEngine: chc // SMTExtCalls: trusted +// SMTIgnoreOS: macos // ---- // Warning 6328: (396-410): CHC: Assertion violation might happen here. // Warning 6328: (429-455): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol b/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol index 8ddef2da9..1298f1f09 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol @@ -17,6 +17,7 @@ function f(uint _x) pure { } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- // Warning 6328: (A:50-64): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call\n A:f(10) -- internal call\n A:f(0) -- internal call // Warning 6328: (s1.sol:28-44): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol b/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol index 42775cc9b..b7b06b1fc 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol @@ -11,5 +11,6 @@ contract C } // ==== // SMTEngine: all +// SMTIgnoreCex: yes // ---- -// Warning 6328: (164-183): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0) +// Warning 6328: (164-183): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_for_bytesNN.sol b/test/libsolidity/smtCheckerTests/operators/index_access_for_bytesNN.sol index 2fee40f40..e73554c1e 100644 --- a/test/libsolidity/smtCheckerTests/operators/index_access_for_bytesNN.sol +++ b/test/libsolidity/smtCheckerTests/operators/index_access_for_bytesNN.sol @@ -6,5 +6,6 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- // Warning 6368: (76-90): CHC: Out of bounds access might happen here. diff --git a/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol b/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol index 91166baa8..7f922105d 100644 --- a/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol +++ b/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol @@ -15,8 +15,11 @@ contract C { assert(g == 0x0001020304050607080900010203040506070809000102030405060708090002); // should fail } } +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes // ---- -// Warning 6328: (225-256): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x0\ne = 0x0\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (352-399): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (526-589): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0102030405060708090001020304050607080900010203\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (732-811): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0102030405060708090001020304050607080900010203\ng = 0x01020304050607080900010203040506070809000102030405060708090001\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (225-256): CHC: Assertion violation happens here. +// Warning 6328: (352-399): CHC: Assertion violation happens here. +// Warning 6328: (526-589): CHC: Assertion violation happens here. +// Warning 6328: (732-811): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/bool_simple_2.sol b/test/libsolidity/smtCheckerTests/types/bool_simple_2.sol index ce35a6505..340d933b8 100644 --- a/test/libsolidity/smtCheckerTests/types/bool_simple_2.sol +++ b/test/libsolidity/smtCheckerTests/types/bool_simple_2.sol @@ -5,5 +5,6 @@ contract C { } // ==== // SMTEngine: all +// SMTIgnoreCex: yes // ---- -// Warning 6328: (66-80): CHC: Assertion violation happens here.\nCounterexample:\n\nx = false\ny = true\n\nTransaction trace:\nC.constructor()\nC.f(false, true) +// Warning 6328: (66-80): CHC: Assertion violation happens here.