k-user AT lists.siebelschool.illinois.edu

Subject: K-user mailing list

List archive

[[K-user] ] How to use the SMT Solver included

From: <jpkratos AT gmail.com>
To: k-user AT lists.cs.illinois.edu
Subject: [[K-user] ] How to use the SMT Solver included
Date: Wed, 16 May 2018 13:06:26 -0500

Hello everyone,

I'm trying to use the SMT Module included in K but it is not available on K
4.0 or K 3.6. However, there is an smt.k file in the 3.4 version of K, but if
I try to import any module in it there is an import error about "builtins/
array-symbolic.k" not being found.

Also, commenting the line importing this builtin, as previous posts suggested,
leaves me with a maude error.

I'm stuck in my research process due to this problem. If anyone can offer any
help I would be very thankful.

[[K-user] ] How to use the SMT Solver included, jpkratos, 05/16/2018