cerc-io/solidity
11
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

regenerating tests expectation

Browse Source
This commit is contained in:
George Plotnikov
2022-10-26 15:13:47 +05:00
parent 376b923a79
commit 6374b4fe23
200 changed files with 9142 additions and 478 deletions
Download Patch File Download Diff File Expand all files Collapse all files
test/cmdlineTests/standard_model_checker_divModSlacks_false_all/output.json
+65 -8
View File
@@ -1,4 +1,9 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x591e1d66214247cc99275e22a55210a804c80e9939d5e515cd60a20b3a927c44":"(set-option :produce-models true)
{
"auxiliaryInputRequested":
{
"smtlib2queries":
{
"0x591e1d66214247cc99275e22a55210a804c80e9939d5e515cd60a20b3a927c44": "(set-option :produce-models true)
(set-logic ALL)
(declare-fun |a_3_3| () Int)
(declare-fun |b_5_3| () Int)
@@ -51,7 +56,8 @@
(assert (= |EVALEXPR_4| expr_19_0))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
","0x5d07befb0482a6d4e328641d57f10a2cbc89b2c287f8d5630bbe20ba4f829e7d":"(set-option :produce-models true)
",
"0x5d07befb0482a6d4e328641d57f10a2cbc89b2c287f8d5630bbe20ba4f829e7d": "(set-option :produce-models true)
(set-logic ALL)
(declare-fun |a_3_3| () Int)
(declare-fun |b_5_3| () Int)
@@ -104,7 +110,8 @@
(assert (= |EVALEXPR_4| expr_22_0))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
","0x72b32f47722af7f889ab5740b229c1799f27d0a693995a581c00f65438255a15":"(set-option :produce-models true)
",
"0x72b32f47722af7f889ab5740b229c1799f27d0a693995a581c00f65438255a15": "(set-option :produce-models true)
(set-logic ALL)
(declare-fun |a_3_3| () Int)
(declare-fun |b_5_3| () Int)
@@ -136,7 +143,8 @@
(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 (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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)))
(check-sat)
","0x825b322db572f1c2705128460f2af503aeeb571f1c2e15207ce4fd0355accee6":"(set-option :produce-models true)
",
"0x825b322db572f1c2705128460f2af503aeeb571f1c2e15207ce4fd0355accee6": "(set-option :produce-models true)
(set-logic ALL)
(declare-fun |a_3_3| () Int)
(declare-fun |b_5_3| () Int)
@@ -168,18 +176,67 @@
(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 (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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))
(check-sat)
"}},"errors":[{"component":"general","errorCode":"1218","formattedMessage":"Warning: CHC: Error trying to invoke SMT solver.
"
}
},
"errors":
[
{
"component": "general",
"errorCode": "1218",
"formattedMessage": "Warning: CHC: Error trying to invoke SMT solver.
--> A:7:15:
|
7 | \t\t\t\t\t\treturn (a / b, a % b);
| \t\t\t\t\t\t ^^^^^
","message":"CHC: Error trying to invoke SMT solver.","severity":"warning","sourceLocation":{"end":182,"file":"A","start":177},"type":"Warning"},{"component":"general","errorCode":"1218","formattedMessage":"Warning: CHC: Error trying to invoke SMT solver.
",
"message": "CHC: Error trying to invoke SMT solver.",
"severity": "warning",
"sourceLocation":
{
"end": 182,
"file": "A",
"start": 177
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "1218",
"formattedMessage": "Warning: CHC: Error trying to invoke SMT solver.
--> A:7:22:
|
7 | \t\t\t\t\t\treturn (a / b, a % b);
| \t\t\t\t\t\t ^^^^^
","message":"CHC: Error trying to invoke SMT solver.","severity":"warning","sourceLocation":{"end":189,"file":"A","start":184},"type":"Warning"},{"component":"general","errorCode":"5840","formattedMessage":"Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
",
"message": "CHC: Error trying to invoke SMT solver.",
"severity": "warning",
"sourceLocation":
{
"end": 189,
"file": "A",
"start": 184
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "5840",
"formattedMessage": "Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
","message":"CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}
",
"message": "CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.",
"severity": "warning",
"type": "Warning"
}
],
"sources":
{
"A":
{
"id": 0
}
}
}