getNextExit-spec.k

getNextExit spec error

.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