k-legacy icon indicating copy to clipboard operation
k-legacy copied to clipboard

krun prints out a warning when taking the "size" of a list containing a single element

Open dfava opened this issue 8 years ago • 0 comments

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

dfava avatar Feb 21 '17 15:02 dfava