SPEC ERROR: /Users/chrissmith/Projects/k-ds-guard/out/specs/617021af8de987b5d4f7d2a2afac1a72fd17c33b75cdc5f1440117d544b77a8e.k Location(12,3,180,36)
==================================
Success execution paths: 0
Failed execution paths: 1
Paths in progress: 1
Longest path: 131 steps
Stats for each phase, time, used memory, implicit main GC time percentage:
Total : 218.558 s, 541 MB, gc: 0.649 %
Parsing : 206.018 s, 135 MB, gc: 0.610 %
Init : 1.854 s, 485 MB, gc: 0.917 %
Execution : 10.685 s, 541 MB, gc: 1.357 %
Init+Execution time: 12.539 s
query build time : 0.072 s, # 67
Z3 Regular rule implication time : 0.305 s, # 16
unsat (proved): 16
cached queries: 2
Z3 Function rule implication time: 0.231 s, # 10
unknown : 10
cached queries: 2
Z3 Spec rule implication time : 0.015 s, # 1
unsat (proved): 1
Z3 Regular rule constraint time : 0.749 s, # 39
unknown : 21
unsat (proved): 17
Z3 Spec rule constraint time : 0.021 s, # 1
unknown : 1
Time and top-level event counts:
resolveFunctionAndAnywhere time : 1.654 s, # 3610
evaluateFunction time : 1.640 s, # 777
builtin evaluation : , # 127
function rule : , # 151
sort predicate : , # 56
no rule applicable : , # 443
applyAnywhereRules time : 0.001 s, # 2083
no anywhere rules : , # 2083
remaining time & # cached : 0.013 s, # 750
impliesSMT time : 0.592 s, # 31
Recursive event counts:
resolveFunctionAndAnywhere time : , # 94100
evaluateFunction time : , # 42311
builtin evaluation : , # 23852
function rule : , # 18278
sort predicate : , # 69
no rule applicable : , # 107
applyAnywhereRules time : , # 9021
no anywhere rules : , # 9021
# cached : , # 42768
Max memory : 10240 MB
==================================
[Error] Critical: Z3 crashed on input query:
(declare-sort WordStack)
(declare-sort KItem)
(declare-fun asByteStack (Int WordStack) WordStack)
(declare-fun asWord (WordStack) Int)
(declare-fun buf (Int Int) WordStack)
(declare-fun sizeWordStack (WordStack) Int)
(declare-fun _dotWS () WordStack)
(declare-fun _plusWS_ (WordStack WordStack) WordStack)
(declare-fun _WS_ (Int WordStack) WordStack)
(declare-fun chop (Int) Int)
(declare-fun smt_keccak (WordStack) Int)
(declare-fun smt_nthbyteof (Int Int Int) Int)
(declare-fun sizeWordStackAux (WordStack Int) Int)
(assert (forall ((|R_I_260| Int)) (= (chop |R_I_260|) (mod |R_I_260| 115792089237316195423570985008687907853269984665640564039457584007913129639936))))
(assert (forall ((|R__0_298| WordStack)(|R__1_299| Int)) (= (>= (sizeWordStackAux |R__0_298| |R__1_299|) 0) true)))
(declare-fun |CD_1572| () WordStack)
(declare-fun |R_CD| () WordStack)
(declare-fun |ACCT_ID_1570| () Int)
(declare-fun |CALLER_ID_1648| () Int)
(declare-fun |ORIGIN_ID_1561| () Int)
(declare-fun |TIME_1638| () Int)
(declare-fun |ACCT_ID_balance_1562| () Int)
(declare-fun |ECREC_BAL_1560| () Int)
(declare-fun |SHA256_BAL_1571| () Int)
(declare-fun |RIP160_BAL_1649| () Int)
(declare-fun |ID_BAL_1559| () Int)
(declare-fun |MODEXP_BAL_1564| () Int)
(declare-fun |ECADD_BAL_1642| () Int)
(declare-fun |ECMUL_BAL_1563| () Int)
(declare-fun |ECPAIRING_BAL_1641| () Int)
(declare-fun |VCallDepth_1643| () Int)
(declare-fun |ABI_src_1569| () Int)
(declare-fun |Can_1583| () Int)
(declare-fun |VGas_1639| () Int)
(declare-fun |_3000| () KItem)
(assert (and
(= (_plusWS_ _3000 |CD_1572|) |R_CD|)
(= (<= 0 |ACCT_ID_1570|) true)
(= (<= |ACCT_ID_1570| 1461501637330902918203684832716283019655932542975) true)
(= (< 0 |ACCT_ID_1570|) true)
(= (<= 9 |ACCT_ID_1570|) true)
(= (<= 0 |CALLER_ID_1648|) true)
(= (<= |CALLER_ID_1648| 1461501637330902918203684832716283019655932542975) true)
(= (<= 0 |ORIGIN_ID_1561|) true)
(= (<= |ORIGIN_ID_1561| 1461501637330902918203684832716283019655932542975) true)
(= (<= 0 |TIME_1638|) true)
(= (<= |TIME_1638| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |ACCT_ID_balance_1562|) true)
(= (<= |ACCT_ID_balance_1562| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |ECREC_BAL_1560|) true)
(= (<= |ECREC_BAL_1560| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |SHA256_BAL_1571|) true)
(= (<= |SHA256_BAL_1571| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |RIP160_BAL_1649|) true)
(= (<= |RIP160_BAL_1649| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |ID_BAL_1559|) true)
(= (<= |ID_BAL_1559| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |MODEXP_BAL_1564|) true)
(= (<= |MODEXP_BAL_1564| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |ECADD_BAL_1642|) true)
(= (<= |ECADD_BAL_1642| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |ECMUL_BAL_1563|) true)
(= (<= |ECMUL_BAL_1563| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |ECPAIRING_BAL_1641|) true)
(= (<= |ECPAIRING_BAL_1641| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= |VCallDepth_1643| 1024) true)
(= (<= 0 |ABI_src_1569|) true)
(= (<= |ABI_src_1569| 1461501637330902918203684832716283019655932542975) true)
(= (<= 0 |Can_1583|) true)
(= (<= |Can_1583| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= (sizeWordStackAux |CD_1572| 0) 1250000000) true)
(= (>= |VGas_1639| 3000000) true)))
result:
(error "line 114 column 29: Sort mismatch at argument #1 for function (declare-fun _plusWS_ (WordStack WordStack) WordStack) supplied sort is KItem")
unknown
while checking satisfiability for:
ConjunctiveFormula(
substitutions:
_==K_(ABI_dst_1567:Int,, ABI_src_1569:Int)
_==K_(R_DotVar1:K,, #KSequence(#pc[_]_EVM(CALLDATASIZE_EVM(.KList)), #execute_EVM(.KList), CONTINUATION_1647:K))
_==K_(VCallValue_1645:Int,, Int(#"0"))
equalities:
_==K_(_++_WS(#abiCallData(String(#""canCall""),, typedArgs(#address(ABI_src_1569:Int),, typedArgs(#address(ABI_src_1569:Int),, typedArgs(#bytes4(ABI_sig_1568:Int),, .List{"typedArgs"}(.KList))))),, CD_1572:WordStack),, R_CD:WordStack)
_==K_(_<=Int_(ABI_src_1569:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
_==K_(_<=Int_(ACCT_ID_1570:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
_==K_(_<=Int_(ACCT_ID_balance_1562:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(CALLER_ID_1648:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
_==K_(_<=Int_(Can_1583:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ECADD_BAL_1642:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ECMUL_BAL_1563:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ECPAIRING_BAL_1641:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ECREC_BAL_1560:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ID_BAL_1559:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ABI_src_1569:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ACCT_ID_1570:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ACCT_ID_balance_1562:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, CALLER_ID_1648:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, Can_1583:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ECADD_BAL_1642:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ECMUL_BAL_1563:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ECPAIRING_BAL_1641:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ECREC_BAL_1560:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ID_BAL_1559:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, MODEXP_BAL_1564:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ORIGIN_ID_1561:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, RIP160_BAL_1649:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, SHA256_BAL_1571:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, TIME_1638:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"9"),, ACCT_ID_1570:Int),, Bool(#"true"))
_==K_(_<=Int_(MODEXP_BAL_1564:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ORIGIN_ID_1561:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
_==K_(_<=Int_(RIP160_BAL_1649:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(SHA256_BAL_1571:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(TIME_1638:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(VCallDepth_1643:Int,, Int(#"1024")),, Bool(#"true"))
_==K_(_<=Int_(sizeWordStackAux(CD_1572:WordStack,, Int(#"0")),, Int(#"1250000000")),, Bool(#"true"))
_==K_(_<Int_(Int(#"0"),, ACCT_ID_1570:Int),, Bool(#"true"))
_==K_(_>=Int_(VGas_1639:Int,, Int(#"3000000")),, Bool(#"true"))
)
Created
July 16, 2019 23:56
-
-
Save iamchrissmith/7a4635c5dbe21bf40d0c22ebc308159f to your computer and use it in GitHub Desktop.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment