cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #10851 from blishko/smt-address-constraints

Browse Source 
[SMTChecker] Add missing type constraints for Address
This commit is contained in:
Leonardo 2021-01-28 10:06:32 +01:00 committed by GitHub
commit 73b9a03f21
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
35 changed files with 846 additions and 823 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
libsolidity/formal/SymbolicTypes.cpp
View File

@ -426,7 +426,7 @@ smtutil::Expression maxValue(frontend::TypePointer _type)
)
return TypeProvider::uint(160)->maxValue();
if (auto const* enumType = dynamic_cast<EnumType const*>(_type))
return enumType->numberOfMembers();
return enumType->numberOfMembers() - 1;
if (auto const* bytesType = dynamic_cast<FixedBytesType const*>(_type))
return TypeProvider::uint(bytesType->numBytes() * 8)->maxValue();
solAssert(false, "");
@ -544,18 +544,8 @@ void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer co
smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::TypePointer const& _type)
{
solAssert(_type, "");
if (isEnum(*_type))
{
auto enumType = dynamic_cast<frontend::EnumType const*>(_type);
solAssert(enumType, "");
return _expr >= 0 && _expr < enumType->numberOfMembers();
}
else if (isInteger(*_type))
{
auto intType = dynamic_cast<frontend::IntegerType const*>(_type);
solAssert(intType, "");
return _expr >= minValue(*intType) && _expr <= maxValue(*intType);
}
if (isEnum(*_type) || isInteger(*_type) || isAddress(*_type) || isFixedBytes(*_type))
return _expr >= minValue(_type) && _expr <= maxValue(_type);
else if (isArray(*_type) || isMapping(*_type))
/// Length cannot be negative.
return smtutil::Expression::tuple_get(_expr, 1) >= 0;

4
test/cmdlineTests/standard_model_checker_engine_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x1b0b95f75c7c1f14af97d9682c4b88edc51efc5b3bb09e7fd6f39bc6274879d7":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x3dd1badc478531aafa4f9308fc524a6530c0623bdff8afe13266e1804c3418f5":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -17,7 +17,7 @@
(declare-fun |expr_9_0| () Int)
(declare-fun |expr_10_1| () Bool)
(assert (and (and (and true true) (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (implies (and true true) true) (and (= expr_9_0 0) (and (implies (and true true) (and (>= expr_8_0 0) (<= expr_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 3017696395)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))) (not expr_10_1)))
(assert (and (and (and true true) (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (implies (and true true) true) (and (= expr_9_0 0) (and (implies (and true true) (and (>= expr_8_0 0) (<= expr_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 3017696395)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))) (not expr_10_1)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_4_0))
(check-sat)

58
test/cmdlineTests/standard_model_checker_targets_all/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x2eb38749740acf428ef329267494f14140859daaad71e856199ee8dc9e4b0eea":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x08b5795f9eda8ce53446419950994fabcdc4bd3534d92074097a1b534a7a7272":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -21,34 +21,9 @@
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) expr_15_1))
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) expr_15_1))
(check-sat)
","0x4c58222d2cbbb4886e8c7bc6a52fc5201b4f03e11a8f7c750a04c4e561184543":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
(declare-fun |state_0| () |state_type|)
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
(declare-fun |tx_0| () |tx_type|)
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
(declare-fun |crypto_0| () |crypto_type|)
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) (not expr_15_1)))
(check-sat)
","0x6a1f744bce6c40be2bb493e9488ed83fa2d6c0a40726e9039bbc29d191eb8845":"(set-option :produce-models true)
","0xa3a9a85c7313ac3a80a77a38a35668db7068ee2f7be140badd368376fc37aee8":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -95,13 +70,38 @@
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) true) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_12_0)) (and (and (<= 0 r_div_mod_12_0) (or (= expr_30_0 0) (< r_div_mod_12_0 expr_30_0))) (and (= (+ (* d_div_mod_12_0 expr_30_0) r_div_mod_12_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) (and (>= expr_33_0 0) (<= expr_33_0 1461501637330902918203684832716283019655932542975))) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_12_0)) (and (and (<= 0 r_div_mod_12_0) (or (= expr_30_0 0) (< r_div_mod_12_0 expr_30_0))) (and (= (+ (* d_div_mod_12_0 expr_30_0) r_div_mod_12_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_1))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| ))
","0xf2731599635c133039b4b9b9e9900964e0192a6fe64c6e4725f2b822922cbc7c":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
(declare-fun |state_0| () |state_type|)
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
(declare-fun |tx_0| () |tx_type|)
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
(declare-fun |crypto_0| () |crypto_type|)
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) (not expr_15_1)))
(check-sat)
"}},"errors":[{"component":"general","errorCode":"3944","formattedMessage":"Warning: CHC: Underflow (resulting value less than 0) happens here.
Counterexample:
arr = []

336
test/cmdlineTests/standard_model_checker_targets_all_bmc/output.json
View File

File diff suppressed because one or more lines are too long

4
test/cmdlineTests/standard_model_checker_targets_assert_bmc/output.json
View File

File diff suppressed because one or more lines are too long

4
test/cmdlineTests/standard_model_checker_targets_balance_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x240e234b94730ae77186055cfd497955c31eb06962d89249b2586d5fb787507b":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x9b94a8878934c648564a23da56d4cc9579313c23abc8692b88b1782d817acde2":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -45,7 +45,7 @@
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) true) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_30_0 0) (< r_div_mod_0_0 expr_30_0))) (and (= (+ (* d_div_mod_0_0 expr_30_0) r_div_mod_0_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) (and (>= expr_33_0 0) (<= expr_33_0 1461501637330902918203684832716283019655932542975))) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_30_0 0) (< r_div_mod_0_0 expr_30_0))) (and (= (+ (* d_div_mod_0_0 expr_30_0) r_div_mod_0_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(declare-const |EVALEXPR_1| Int)

8
test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x2eb38749740acf428ef329267494f14140859daaad71e856199ee8dc9e4b0eea":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x08b5795f9eda8ce53446419950994fabcdc4bd3534d92074097a1b534a7a7272":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -21,9 +21,9 @@
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) expr_15_1))
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) expr_15_1))
(check-sat)
","0x4c58222d2cbbb4886e8c7bc6a52fc5201b4f03e11a8f7c750a04c4e561184543":"(set-option :produce-models true)
","0xf2731599635c133039b4b9b9e9900964e0192a6fe64c6e4725f2b822922cbc7c":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -46,7 +46,7 @@
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) (not expr_15_1)))
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))) (not expr_15_1)))
(check-sat)
"}},"errors":[{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
--> A:7:15:

4
test/cmdlineTests/standard_model_checker_targets_div_by_zero_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x8a2330735f961222d4ded7523ff3ddd71f2967f10f056fbebb244ece16e5c9f3":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x2efabbc36c3f3b25f5f8725e7842db652874a0f4688f1499bd02338eb5a8e474":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -45,7 +45,7 @@
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))))))))) (= expr_30_0 0)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))))))))) (= expr_30_0 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(declare-const |EVALEXPR_1| Int)

4
test/cmdlineTests/standard_model_checker_targets_overflow_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x7f46266457e86907efcdec9266c9a8c23d52471a5a83a51b4cbdbabd6bcc8448":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x42284231a02038ba8e0e3314ca51e23df497864639e1950130e96296e4ff2a3e":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -45,7 +45,7 @@
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))) (> (+ expr_21_0 expr_26_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))) (> (+ expr_21_0 expr_26_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(declare-const |EVALEXPR_1| Int)

4
test/cmdlineTests/standard_model_checker_targets_underflow_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x26cdd5a03c30ad821b02bb2a01dd93315bbb5a2ac7625639a97c9163b532d3cf":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0xfd788cde742658cd0e4ab59ecdad2cfdf2afc4442e13f50faae7aaf05062cc44":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -45,7 +45,7 @@
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true))))))))))))) (< (- x_9_0 1) 0)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true))))))))))))) (< (- x_9_0 1) 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(declare-const |EVALEXPR_1| Int)

24
test/cmdlineTests/standard_model_checker_targets_underflow_overflow_assert_bmc/output.json
View File

File diff suppressed because one or more lines are too long

116
test/cmdlineTests/standard_model_checker_targets_underflow_overflow_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x26cdd5a03c30ad821b02bb2a01dd93315bbb5a2ac7625639a97c9163b532d3cf":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x42284231a02038ba8e0e3314ca51e23df497864639e1950130e96296e4ff2a3e":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -45,63 +45,7 @@
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true))))))))))))) (< (- x_9_0 1) 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_0))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| (- x_9_0 1)))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
","0x7f46266457e86907efcdec9266c9a8c23d52471a5a83a51b4cbdbabd6bcc8448":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
(declare-fun |state_0| () |state_type|)
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
(declare-fun |tx_0| () |tx_type|)
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
(declare-fun |crypto_0| () |crypto_type|)
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_1| () Int)
(declare-fun |x_9_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_0| () Int)
(declare-fun |expr_42_1| () Bool)
(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) true) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))) (> (+ expr_21_0 expr_26_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- x_9_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- x_9_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true)))))))))))))))))))) (> (+ expr_21_0 expr_26_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(declare-const |EVALEXPR_1| Int)
@ -110,6 +54,62 @@
(assert (= |EVALEXPR_2| (+ expr_21_0 expr_26_1)))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
","0xfd788cde742658cd0e4ab59ecdad2cfdf2afc4442e13f50faae7aaf05062cc44":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
(declare-fun |state_0| () |state_type|)
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
(declare-fun |tx_0| () |tx_type|)
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
(declare-fun |crypto_0| () |crypto_type|)
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_1| () Int)
(declare-fun |x_9_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_0| () Int)
(declare-fun |expr_42_1| () Bool)
(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_3| () |uint[]_tuple|)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.sig| tx_0) 1917212865)) (= (|msg.value| tx_0) 0)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4)) true))))))))))))) (< (- x_9_0 1) 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_0))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| (- x_9_0 1)))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
"}},"errors":[{"component":"general","errorCode":"4144","formattedMessage":"Warning: BMC: Underflow (resulting value less than 0) happens here.
--> A:8:7:
|

222
test/cmdlineTests/standard_model_checker_timeout_all/output.json
View File

File diff suppressed because one or more lines are too long

792
test/cmdlineTests/standard_model_checker_timeout_bmc/output.json
View File

File diff suppressed because one or more lines are too long

3
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol
View File

@ -8,5 +8,4 @@ contract C {
}
}
// ----
// Warning 6328: (326-356): CHC: Assertion violation might happen here.
// Warning 7812: (326-356): BMC: Assertion violation might happen here.
// Warning 6328: (326-356): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_3d.sol
View File

@ -25,5 +25,7 @@ contract C {
assert(c[length1 - 1][length2 - 1][length3 - 1] == 200);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (570-625): CHC: Assertion violation happens here.\nCounterexample:\nc = [[[2]]]\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g()
// Warning 6328: (570-625): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol
View File

@ -10,4 +10,4 @@ contract C {
}
}
// ----
// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 2437\n\nTransaction trace:\nC.constructor()\nC.f(2437)
// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 21238\n\nTransaction trace:\nC.constructor()\nC.f(21238)

2
test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
View File

@ -29,7 +29,7 @@ contract C {
// Warning 6328: (305-321): CHC: Assertion violation might happen here.
// Warning 1218: (448-464): CHC: Error trying to invoke SMT solver.
// Warning 6328: (448-464): CHC: Assertion violation might happen here.
// Warning 6328: (673-689): CHC: Assertion violation happens here.\nCounterexample:\n\nh0 = 21238\nv0 = 173\nr0 = 30612\ns0 = 32285\nh1 = 7719\nv1 = 21\nr1 = 10450\ns1 = 8855\n\nTransaction trace:\nC.constructor()\nC.e(21238, 173, 30612, 32285, 7719, 21, 10450, 8855)
// Warning 6328: (673-689): CHC: Assertion violation happens here.\nCounterexample:\n\nh0 = 7719\nv0 = 21\nr0 = 10450\ns0 = 8365\nh1 = 38\nv1 = 151\nr1 = 32285\ns1 = 2437\n\nTransaction trace:\nC.constructor()\nC.e(7719, 21, 10450, 8365, 38, 151, 32285, 2437)
// Warning 4661: (168-184): BMC: Assertion violation happens here.
// Warning 4661: (305-321): BMC: Assertion violation happens here.
// Warning 4661: (448-464): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol
View File

@ -11,4 +11,4 @@ contract C {
}
}
// ----
// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(data)\n C.fi(data, 2437) -- internal call
// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(data)\n C.fi(data, 7719) -- internal call

4
test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
View File

@ -51,7 +51,9 @@ contract C {
// Warning 6328: (749-768): CHC: Assertion violation might happen here.
// Warning 1218: (772-791): CHC: Error trying to invoke SMT solver.
// Warning 6328: (772-791): CHC: Assertion violation might happen here.
// Warning 6328: (795-814): CHC: Assertion violation happens here.
// Warning 1218: (795-814): CHC: Error trying to invoke SMT solver.
// Warning 6328: (795-814): CHC: Assertion violation might happen here.
// Warning 4661: (726-745): BMC: Assertion violation happens here.
// Warning 4661: (749-768): BMC: Assertion violation happens here.
// Warning 4661: (772-791): BMC: Assertion violation happens here.
// Warning 4661: (795-814): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
View File

@ -14,4 +14,6 @@ contract C
// ====
// SMTSolvers: z3
// ----
// Warning 4984: (176-181): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (189-203): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 14\n\nTransaction trace:\nC.constructor()\nC.f(4)
// Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

2
test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol
View File

@ -15,4 +15,4 @@ contract C
// SMTSolvers: z3
// ----
// Warning 5740: (120-123): Unreachable code.
// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\n\nTransaction trace:\nC.constructor()\nC.f(3)
// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(1)

2
test/libsolidity/smtCheckerTests/overflow/overflow_mul_cex_with_array.sol
View File

@ -7,4 +7,4 @@ contract C {
}
}
// ----
// Warning 4984: (118-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = [14, 14, 14, 14, 14, 14, 14, 14, 14, 11, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14]\ny = 23158417847463239084714197001737581570653996933128112807891516801582625927988\n\nTransaction trace:\nC.constructor()\nC.f([14, 14, 14, 14, 14, 14, 14, 14, 14, 11, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14], 23158417847463239084714197001737581570653996933128112807891516801582625927988)
// Warning 4984: (118-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\ny = 23158417847463239084714197001737581570653996933128112807891516801582625927988\n\nTransaction trace:\nC.constructor()\nC.f(x, 23158417847463239084714197001737581570653996933128112807891516801582625927988)

2
test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
View File

@ -14,6 +14,6 @@ contract C {
// Warning 2072: (184-188): Unused local variable.
// Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)
// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 13, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16]\n\nTransaction trace:\nC.constructor()\nC.f([16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 13, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16])
// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10]\n\nTransaction trace:\nC.constructor()\nC.f([10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10])
// Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)

4
test/libsolidity/smtCheckerTests/special/blockhash.sol
View File

@ -10,5 +10,5 @@ contract C
}
}
// ----
// Warning 6328: (85-109): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 7719\n\nTransaction trace:\nC.constructor()\nC.f(7719){ value: 21238 }
// Warning 6328: (113-137): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 7719\n\nTransaction trace:\nC.constructor()\nC.f(7719){ value: 2437 }
// Warning 6328: (85-109): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 7719 }
// Warning 6328: (113-137): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 21238 }

4
test/libsolidity/smtCheckerTests/special/msg_data.sol
View File

@ -22,5 +22,5 @@ contract C
}
}
// ----
// Warning 6328: (153-180): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 8365 }
// Warning 6328: (500-527): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g(){ value: 8365 }
// Warning 6328: (153-180): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 10450 }
// Warning 6328: (500-527): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g(){ value: 10450 }

2
test/libsolidity/smtCheckerTests/special/msg_sender_fail_1.sol
View File

@ -10,4 +10,4 @@ contract C
}
}
// ----
// Warning 6328: (155-178): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 38\n\nTransaction trace:\nC.constructor()\nC.f(38)
// Warning 6328: (155-178): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 39\n\nTransaction trace:\nC.constructor()\nC.f(39)

9
test/libsolidity/smtCheckerTests/special/msg_sender_range.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C {
function f() public view {
assert(msg.sender >= address(0)); // should hold
assert(msg.sender <= address(2**160-1)); // should hold
}
}

2
test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_fixed_bytes.sol
View File

@ -14,4 +14,4 @@ contract C {
}
}
// ----
// Warning 6328: (250-294): CHC: Assertion violation happens here.
// Warning 6328: (250-294): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n C.g() -- trusted external call

2
test/libsolidity/smtCheckerTests/types/array_branch_1d.sol
View File

@ -11,4 +11,4 @@ contract C
}
}
// ----
// Warning 6328: (176-192): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 11]\n\nTransaction trace:\nC.constructor()\nC.f(false, [38, 11])
// Warning 6328: (176-192): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 8]\n\nTransaction trace:\nC.constructor()\nC.f(false, [38, 8])

9
test/libsolidity/smtCheckerTests/types/enum_range.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract C
{
enum D { Left, Right }
function f(D a) public pure {
assert(a == D.Left || a == D.Right);
}
}

2
test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol
View File

@ -6,4 +6,4 @@ contract C {
}
}
// ----
// Warning 4281: (117-120): CHC: Division by zero happens here.\nCounterexample:\n\nx = [14, 14, 14, 14, 14, 14, 14, 14, 14, 11, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14]\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f([14, 14, 14, 14, 14, 14, 14, 14, 14, 11, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14], 0)
// Warning 4281: (117-120): CHC: Division by zero happens here.\nCounterexample:\n\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(x, 0)

10
test/libsolidity/smtCheckerTests/types/fixed_bytes_range.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
function f(bytes1 b) public pure {
bytes1 c = hex"7f";
require(b > c);
assert(uint8(b) > 127); // should hold
}
}

2
test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol
View File

@ -12,4 +12,4 @@ contract c {
}
}
// ----
// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21238\n\nTransaction trace:\nc.constructor()\nc.g(38, 21238)\n c.f(map, 38, 21238) -- internal call
// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21239\n\nTransaction trace:\nc.constructor()\nc.g(38, 21239)\n c.f(map, 38, 21239) -- internal call

2
test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol
View File

@ -10,5 +10,5 @@ contract C {
}
}
// ----
// Warning 6328: (147-166): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293569\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293569)
// Warning 6328: (147-166): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0\n\nTransaction trace:\nC.constructor()\nC.f(0)
// Warning 6328: (170-190): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538830022687173130149211684818290356179572910782152375644828738034597888\n\nTransaction trace:\nC.constructor()\nC.f(52647538830022687173130149211684818290356179572910782152375644828738034597888)