k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[[K-user] ] missing SMTLib translation

From: 璟临天下 <qjq793437528 AT 163.com>
To: k-user <k-user AT lists.cs.illinois.edu>
Subject: [[K-user] ] missing SMTLib translation
Date: Fri, 19 Oct 2018 21:21:09 +0800 (CST)
Authentication-results: illinois.edu; spf=none smtp.mailfrom=qjq793437528 AT 163.com; dkim=pass header.d=163.com header.s=s110527; dmarc=none

Hi all,

I'm defining the operational semantics of a language on K5, and kompile it with option --backend java. when i try to running example programs, there is a warning message as follow:

[Warning] Critical: missing SMTLib translation for
isIntType(_)_PREDICATE-SYNTAX (missing SMTLib translation for
isIntType(_)_PREDICATE-SYNTAX)

does anyone know what is it, and how can i fix this? Thanks for your reading and help.

Best,

Dexter

[[K-user] ] missing SMTLib translation, 璟临天下, 10/19/2018