k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

From: wang_feng_bro AT 163.com
To: k-user AT lists.cs.illinois.edu
Subject: [[K-user] ] Smtlib expression
Date: Mon, 7 Aug 2017 17:03:02 +0800
Authentication-results: illinois.edu; spf=pass smtp.mailfrom=wang_feng_bro AT 163.com

Hi all,

K framework gives a strange warning when running my code(Kompile is ok):

[Warning] Critical: failed to translate smtlib _expression_:

(declare-sort Map)

(declare-sort KItem)

(declare-fun R__41 () Map)

(declare-fun _237 () KItem)

(assert (and (= _237 R__41))

Does anyone met this before ? How to eliminate it ?

Jerry