k-legacy
k-legacy copied to clipboard
krun prints out a warning when taking the "size" of a list containing a single element
krun prints out the following warnings when taking the size of a list containing a single element:
[Warning] Critical: failed to translate smtlib expression:
(assert (and (= (> (smt_seq_len (smt_seq_elem true)) 0) true)))
(error "line 1 column 51: unknown function/constant smt_seq_elem")
(error "line 1 column 51: unknown function/constant smt_seq_elem")
Here is a small definition file that can be used to reproduce the issue: $ cat warn.k
module WARN-SYNTAX
syntax Id ::= "x" | "y" | "z" | "$x"
syntax Val ::= Id | Int
syntax Pgm ::= Val | "load" Id
syntax KResult ::= Val
endmodule
module WARN
imports WARN-SYNTAX
syntax KVariable ::= Id
configuration <T color="yellow">
<k color="green"> $PGM:Pgm </k>
<S color="Orchid"> ListItem( true ) </S>
</T>
rule <k> load Z:Id => 42 </k>
<S> L:List </S>
requires size(L) >Int 0
endmodule
The test file is a one liner: $ cat test.q2 load x
Here is a copy/paste from the krun execution: $ krun test.q2 --debug | pprint
[Warning] Critical: failed to translate smtlib expression:
(assert (and (= (> (smt_seq_len (smt_seq_elem true)) 0) true)))
(error "line 1 column 51: unknown function/constant smt_seq_elem")
(error "line 1 column 51: unknown function/constant smt_seq_elem")
<T>
<k> 42 </k>
<S> ListItem ( true ) </S>
</T>
This issue happens on a pretty recent commit of K: commit 35df078e85e83f23d1b45e7eee5481a8cb9e8939