gistfile1.txt

module SIMPLE-SYNTAX

endmodule

module SIMPLE
  
  imports BOOL
  imports INT

  syntax S ::= "mul(" S "," S ")"
             | Int

  rule mul( X:Int , Y:Int ) => X *Int Y

endmodule

----------------------

module SIMPLE-SPEC
    imports SIMPLE

    rule <k> mul( X , 0 ) => 0 </k>

endmodule

------------------------

# kprove simple-spec.k
[WARNING] Running as root is not recommended
kore-exec: Quantifying both the term and the predicate probably means that there's
an error somewhere else.
variable=VarX0:SortInt{}
patt=\and{SortGeneratedTopCell{}}(
    /* term: */
    Lbl'-LT-'generatedTop'-GT-'{}(
        Lbl'-LT-'k'-GT-'{}(
            kseq{}(
                inj{SortInt{}, SortKItem{}}(
                    Lbl'UndsStar'Int'Unds'{}(
                        VarX0:SortInt{},
                        /* builtin: */ \dv{SortInt{}}("0")
                    )
                ),
                dotk{}()
            )
        ),
        VarDotVar0:SortGeneratedCounterCell{}
    ),
\and{SortGeneratedTopCell{}}(
    /* predicate: */
    \top{SortGeneratedTopCell{}}(),
    /* substitution: */
    \equals{SortS{}, SortGeneratedTopCell{}}(
        VarX:SortS{},
        inj{SortInt{}, SortS{}}(VarX0:SortInt{})
    )
)
)

CallStack (from HasCallStack):
  error, called at src/Kore/Step/Simplification/Exists.hs:316:6 in kore-0.0.1.0-1PYkDqc0weFIAwvx8ImQ2c:Kore.Step.Simplification.Exists
[Error] Internal: Uncaught exception thrown of type FileNotFoundException.
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
(./.kprove-2019-10-25-20-06-27-723-0d22ac6d-6881-4bda-ba67-dd96a9b573eb/result.kore
(No such file or directory))