Skip to content

Commit 2faf8c6

Browse files
author
Leonardo
authored
Merge pull request #11776 from ethereum/smt_fix_constants
[SMTChecker] Fix ICE when running on Uniswap V2
2 parents 13b4e15 + 10397e4 commit 2faf8c6

File tree

23 files changed

+406
-259
lines changed

23 files changed

+406
-259
lines changed

‎libsolidity/formal/BMC.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
8080
{
8181
m_solvedTargets = move(_solvedTargets);
8282
m_context.setSolver(m_interface.get());
83-
m_context.clear();
83+
m_context.reset();
8484
m_context.setAssertionAccumulation(true);
8585
m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
8686
createFreeConstants(sourceDependencies(_source));

‎libsolidity/formal/CHC.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -967,7 +967,7 @@ void CHC::resetSourceAnalysis()
967967
m_context.setSolver(smtlib2Interface->smtlib2Interface());
968968
}
969969

970-
m_context.clear();
970+
m_context.reset();
971971
m_context.resetUniqueId();
972972
m_context.setAssertionAccumulation(false);
973973
}

‎libsolidity/formal/EncodingContext.cpp

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -49,12 +49,6 @@ unsigned EncodingContext::newUniqueId()
4949
return m_nextUniqueId++;
5050
}
5151

52-
void EncodingContext::clear()
53-
{
54-
m_variables.clear();
55-
reset();
56-
}
57-
5852
/// Variables.
5953

6054
shared_ptr<SymbolicVariable> EncodingContext::variable(frontend::VariableDeclaration const& _varDecl)

‎libsolidity/formal/SMTEncoder.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3034,6 +3034,15 @@ void SMTEncoder::createFreeConstants(set<SourceUnit const*, ASTNode::CompareByID
30343034
for (auto node: source->nodes())
30353035
if (auto var = dynamic_cast<VariableDeclaration const*>(node.get()))
30363036
createVariable(*var);
3037+
else if (
3038+
auto contract = dynamic_cast<ContractDefinition const*>(node.get());
3039+
contract && contract->isLibrary()
3040+
)
3041+
for (auto var: contract->stateVariables())
3042+
{
3043+
solAssert(var->isConstant(), "");
3044+
createVariable(*var);
3045+
}
30373046
}
30383047

30393048
smt::SymbolicState& SMTEncoder::state()

‎test/cmdlineTests/standard_model_checker_divModSlacks_default_all/output.json

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
1-
{"auxiliaryInputRequested":{"smtlib2queries":{"0x10763dfdad96614fe8fcaf54161ed2be500bbaa57bda8e2d706b675f1290f13b":"(set-option :produce-models true)
1+
{"auxiliaryInputRequested":{"smtlib2queries":{"0xa34579041bed3510aedf3c5d668d439af5c40bbce2c58c14276be21e3336813c":"(set-option :produce-models true)
22
(set-logic ALL)
3+
(declare-fun |a_3_3| () Int)
4+
(declare-fun |b_5_3| () Int)
5+
(declare-fun |_8_3| () Int)
6+
(declare-fun |_10_3| () Int)
37
(declare-fun |error_0| () Int)
48
(declare-fun |this_0| () Int)
59
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
@@ -12,6 +16,10 @@
1216
(declare-fun |crypto_0| () |crypto_type|)
1317
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
1418
(declare-fun |abi_0| () |abi_type|)
19+
(declare-fun |a_3_4| () Int)
20+
(declare-fun |b_5_4| () Int)
21+
(declare-fun |_8_4| () Int)
22+
(declare-fun |_10_4| () Int)
1523
(declare-fun |a_3_0| () Int)
1624
(declare-fun |b_5_0| () Int)
1725
(declare-fun |_8_0| () Int)
@@ -22,8 +30,12 @@
2230

2331
(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1))
2432
(check-sat)
25-
","0xa0332f5d2cf85238fd31e652cfbcc1d2a774996d4d2368d02b71c393eb375f0e":"(set-option :produce-models true)
33+
","0xee99a9e327c7e01c72a32bb73a3d6338ae9c47df718fd1bb11819f1a4d8bc2b8":"(set-option :produce-models true)
2634
(set-logic ALL)
35+
(declare-fun |a_3_3| () Int)
36+
(declare-fun |b_5_3| () Int)
37+
(declare-fun |_8_3| () Int)
38+
(declare-fun |_10_3| () Int)
2739
(declare-fun |error_0| () Int)
2840
(declare-fun |this_0| () Int)
2941
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
@@ -36,6 +48,10 @@
3648
(declare-fun |crypto_0| () |crypto_type|)
3749
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
3850
(declare-fun |abi_0| () |abi_type|)
51+
(declare-fun |a_3_4| () Int)
52+
(declare-fun |b_5_4| () Int)
53+
(declare-fun |_8_4| () Int)
54+
(declare-fun |_10_4| () Int)
3955
(declare-fun |a_3_0| () Int)
4056
(declare-fun |b_5_0| () Int)
4157
(declare-fun |_8_0| () Int)

‎test/cmdlineTests/standard_model_checker_divModSlacks_false_all/output.json

Lines changed: 59 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,9 @@
1-
{"auxiliaryInputRequested":{"smtlib2queries":{"0x10763dfdad96614fe8fcaf54161ed2be500bbaa57bda8e2d706b675f1290f13b":"(set-option :produce-models true)
2-
(set-logic ALL)
3-
(declare-fun |error_0| () Int)
4-
(declare-fun |this_0| () Int)
5-
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
6-
(declare-fun |state_0| () |state_type|)
7-
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
8-
(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)))))
9-
(declare-fun |tx_0| () |tx_type|)
10-
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
11-
(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))))))
12-
(declare-fun |crypto_0| () |crypto_type|)
13-
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
14-
(declare-fun |abi_0| () |abi_type|)
15-
(declare-fun |a_3_0| () Int)
16-
(declare-fun |b_5_0| () Int)
17-
(declare-fun |_8_0| () Int)
18-
(declare-fun |_10_0| () Int)
19-
(declare-fun |expr_13_0| () Int)
20-
(declare-fun |expr_14_0| () Int)
21-
(declare-fun |expr_15_1| () Bool)
22-
23-
(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1))
24-
(check-sat)
25-
","0x55de298588de6547098e62309fe1065399b5711eae0146b256137aa05d54806c":"(set-option :produce-models true)
1+
{"auxiliaryInputRequested":{"smtlib2queries":{"0x503238c9aeac0c67f62d9986977560ad9beb4435de6b6317e104f1342ee2dd14":"(set-option :produce-models true)
262
(set-logic ALL)
3+
(declare-fun |a_3_3| () Int)
4+
(declare-fun |b_5_3| () Int)
5+
(declare-fun |_8_3| () Int)
6+
(declare-fun |_10_3| () Int)
277
(declare-fun |error_0| () Int)
288
(declare-fun |this_0| () Int)
299
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
@@ -36,6 +16,10 @@
3616
(declare-fun |crypto_0| () |crypto_type|)
3717
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
3818
(declare-fun |abi_0| () |abi_type|)
19+
(declare-fun |a_3_4| () Int)
20+
(declare-fun |b_5_4| () Int)
21+
(declare-fun |_8_4| () Int)
22+
(declare-fun |_10_4| () Int)
3923
(declare-fun |a_3_0| () Int)
4024
(declare-fun |b_5_0| () Int)
4125
(declare-fun |_8_0| () Int)
@@ -67,8 +51,44 @@
6751
(assert (= |EVALEXPR_4| expr_22_0))
6852
(check-sat)
6953
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
70-
","0xa0332f5d2cf85238fd31e652cfbcc1d2a774996d4d2368d02b71c393eb375f0e":"(set-option :produce-models true)
54+
","0xa34579041bed3510aedf3c5d668d439af5c40bbce2c58c14276be21e3336813c":"(set-option :produce-models true)
55+
(set-logic ALL)
56+
(declare-fun |a_3_3| () Int)
57+
(declare-fun |b_5_3| () Int)
58+
(declare-fun |_8_3| () Int)
59+
(declare-fun |_10_3| () Int)
60+
(declare-fun |error_0| () Int)
61+
(declare-fun |this_0| () Int)
62+
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
63+
(declare-fun |state_0| () |state_type|)
64+
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
65+
(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)))))
66+
(declare-fun |tx_0| () |tx_type|)
67+
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
68+
(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))))))
69+
(declare-fun |crypto_0| () |crypto_type|)
70+
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
71+
(declare-fun |abi_0| () |abi_type|)
72+
(declare-fun |a_3_4| () Int)
73+
(declare-fun |b_5_4| () Int)
74+
(declare-fun |_8_4| () Int)
75+
(declare-fun |_10_4| () Int)
76+
(declare-fun |a_3_0| () Int)
77+
(declare-fun |b_5_0| () Int)
78+
(declare-fun |_8_0| () Int)
79+
(declare-fun |_10_0| () Int)
80+
(declare-fun |expr_13_0| () Int)
81+
(declare-fun |expr_14_0| () Int)
82+
(declare-fun |expr_15_1| () Bool)
83+
84+
(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1))
85+
(check-sat)
86+
","0xee99a9e327c7e01c72a32bb73a3d6338ae9c47df718fd1bb11819f1a4d8bc2b8":"(set-option :produce-models true)
7187
(set-logic ALL)
88+
(declare-fun |a_3_3| () Int)
89+
(declare-fun |b_5_3| () Int)
90+
(declare-fun |_8_3| () Int)
91+
(declare-fun |_10_3| () Int)
7292
(declare-fun |error_0| () Int)
7393
(declare-fun |this_0| () Int)
7494
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
@@ -81,6 +101,10 @@
81101
(declare-fun |crypto_0| () |crypto_type|)
82102
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
83103
(declare-fun |abi_0| () |abi_type|)
104+
(declare-fun |a_3_4| () Int)
105+
(declare-fun |b_5_4| () Int)
106+
(declare-fun |_8_4| () Int)
107+
(declare-fun |_10_4| () Int)
84108
(declare-fun |a_3_0| () Int)
85109
(declare-fun |b_5_0| () Int)
86110
(declare-fun |_8_0| () Int)
@@ -91,8 +115,12 @@
91115

92116
(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_15_1)))
93117
(check-sat)
94-
","0xab025faeb2e4c20d674670ede4603b61a2424f98dff12acd21022b2ba2d021a2":"(set-option :produce-models true)
118+
","0xf29b8754d9db509b191749e8e885b5ba613be6810511ee7313097ee323e5064c":"(set-option :produce-models true)
95119
(set-logic ALL)
120+
(declare-fun |a_3_3| () Int)
121+
(declare-fun |b_5_3| () Int)
122+
(declare-fun |_8_3| () Int)
123+
(declare-fun |_10_3| () Int)
96124
(declare-fun |error_0| () Int)
97125
(declare-fun |this_0| () Int)
98126
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
@@ -105,6 +133,10 @@
105133
(declare-fun |crypto_0| () |crypto_type|)
106134
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
107135
(declare-fun |abi_0| () |abi_type|)
136+
(declare-fun |a_3_4| () Int)
137+
(declare-fun |b_5_4| () Int)
138+
(declare-fun |_8_4| () Int)
139+
(declare-fun |_10_4| () Int)
108140
(declare-fun |a_3_0| () Int)
109141
(declare-fun |b_5_0| () Int)
110142
(declare-fun |_8_0| () Int)

0 commit comments

Comments
 (0)