Last active
November 8, 2018 08:39
-
-
Save yudetamago/8071c396aadd2d7707d387c71c6fcbc6 to your computer and use it in GitHub Desktop.
getNextExit-spec.k
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
.build/evm-semantics/kevm prove specs/plasma-mvp/getNextExit-spec.k --z3-impl-timeout 500 --verbose | |
Parse command line options = 19 | |
Importing: Source(/mydir/layerx/verified-plasma-contracts/././specs/plasma-mvp/getNextExit-spec.k) | |
Importing: Source(/mydir/layerx/verified-plasma-contracts/specs/plasma-mvp/getNextExit-spec.k) | |
Importing: Source(/mydir/layerx/verified-plasma-contracts/specs/plasma-mvp/abstract-semantics.k) | |
Importing: Source(/mydir/layerx/verified-plasma-contracts/specs/plasma-mvp/verification.k) | |
Importing: Source(/mydir/layerx/verified-plasma-contracts/.build/evm-semantics/.build/java/edsl.k) | |
Importing: Source(/mydir/layerx/verified-plasma-contracts/.build/evm-semantics/.build/java/evm.k) | |
Importing: Source(/mydir/layerx/verified-plasma-contracts/.build/evm-semantics/.build/java/data.k) | |
Importing: Source(/mydir/layerx/verified-plasma-contracts/.build/evm-semantics/.build/java/krypto.k) | |
Importing: Source(/mydir/layerx/verified-plasma-contracts/.build/evm-semantics/.build/java/network.k) | |
Importing: Source(/mydir/layerx/verified-plasma-contracts/specs/lemmas.k) | |
Parsing finished: 30.031 s | |
Initialization finished | |
================================== | |
Total time: 99.822 | |
Parsing time: 30.031 | |
Initialization time: 69.791 | |
Execution time: 0.000 | |
Init+Execution time: 69.791 | |
query build time: 0.018 s | |
Z3 constraint time: 0.000 s | |
Z3 implication time: 1.288 s | |
Z3 implication queries: 10 | |
resolveFunction time: 69.594 s | |
resolveFunction top-level calls: 275 | |
================================== | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 error: (error "line 27 column 586: Sorts K and KItem are incompatible") | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 error: (error "line 27 column 705: Sorts K and KItem are incompatible") | |
z3 likely timeout | |
z3 likely timeout | |
z3 likely timeout | |
z3 error: (error "line 27 column 710: Sorts K and KItem are incompatible") | |
z3 error: (error "line 27 column 710: Sorts K and KItem are incompatible") | |
z3 error: (error "line 28 column 710: Sorts K and KItem are incompatible") | |
z3 error: (error "line 28 column 710: Sorts K and KItem are incompatible") | |
z3 likely timeout | |
z3 likely timeout | |
z3 error: (error "line 28 column 705: Sorts K and KItem are incompatible") | |
z3 likely timeout | |
(...) | |
[Error] Internal: Uncaught exception thrown of type AssertionError. | |
Please rerun your program with the --debug flag to generate a stack trace, and | |
file a bug report at https://github.com/kframework/k/issues (unexpected class | |
at matching: class org.kframework.backend.java.kil.KList) | |
[Warning] Critical: missing SMTLib translation for Set:in (missing SMTLib | |
translation for Set:in) | |
[Warning] Critical: missing SMTLib translation for _in_keys(_)_MAP (missing | |
SMTLib translation for _in_keys(_)_MAP) | |
[Warning] Critical: missing SMTLib translation for isInvalidOp (missing SMTLib | |
translation for isInvalidOp) | |
[Warning] Critical: missing SMTLib translation for log2Int (missing SMTLib | |
translation for log2Int) | |
make: *** [specs/plasma-mvp/getNextExit-spec.k.test] Error 1 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment