SMT Solver call from specification in K 4.0

[daparpon]

Hi! I am interested in checking the validity (by unsatisfiability of a negated expression) of an expression inside a rule of my language specification in K 4.0. I used to implement it in K 3.4 by calling the built-in function "checkSat(K)", which in turn sends the expression to the SMT Solver. However, kompile tells me that this is no longer valid. How could I do it in K 4.0? Thanks in advance.

[dwightguth]

I believe the Java backend has the hook #BOOL:checksat_, but note that it was never tested with K4 and I can't guarantee it will work. SMT functionality was built into the rewriter in more recent versions of K, so explicitly checking satisfiability in rules was not considered a priority and thus not maintained. I would recommend you try to port your semantics to K 5 if it doesn't work, as we do not in any way maintain earlier major releases of K.