K-user mailing list

[Daniel Schnetzer Fava <danielsf AT ifi.uio.no>]

There doesn't seem to be an issue related to this on GitHub.  Would you like me to open one?

I was asked to file an issue on GitHug.  Here it is:

https://github.com/kframework/k/issues/2283

Thank you,

Daniel

On 21 Feb 2017, at 10:12, Daniel Schnetzer Fava <danielsf AT ifi.uio.no> wrote:

Hi,

krun generates the following warning when evaluating a rule with "size(L)" where L is a single element list created with ListItem(Item)

[Warning] Critical: failed to translate smtlib _expression_:
(assert (and (= (< (smt_seq_len (smt_seq_elem true)) 2) true)))
(error "line 1 column 51: unknown function/constant smt_seq_elem")

(error "line 1 column 51: unknown function/constant smt_seq_elem")

Is this expected?

Note that the list items are booleans, thus the (smt_seq_elem true).

There doesn't seem to be an issue related to this on GitHub.  Would you like me to open one?

I am using K-4.0 commit 35df078e85e83f23d1b45e7eee5481a8cb9e8939

Thanks!

Daniel Fava