k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[[K-user] ] [Warning] Critical: failed to translate smtlib expression

From: Daniel Schnetzer Fava <danielsf AT ifi.uio.no>
To: "k-user AT lists.cs.illinois.edu" <k-user AT lists.cs.illinois.edu>
Subject: [[K-user] ] [Warning] Critical: failed to translate smtlib expression
Date: Tue, 21 Feb 2017 09:12:00 +0000
Accept-language: en-US, nb-NO

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

[[K-user] ] [Warning] Critical: failed to translate smtlib expression, Daniel Schnetzer Fava, 02/21/2017
- Re: [[K-user] ] [Warning] Critical: failed to translate smtlib expression, Daniel Schnetzer Fava, 02/21/2017