K-user mailing list

[<daparpon AT dsic.upv.es>]

Hi! I managed to call the SMT Solver from a K specification and obtain a
result, through the expression with profile "checkSat(Bool) -> String".
However, the result provided does not match the expected one for my particular
test case: Z3 returns "unknown" during K execution, but when I tried out the
same operation in the web application of Z3 at rise4fun
(http://rise4fun.com/Z3), I got "unsat", which is the result that I expected.

The boolean expression that causes this conflict is packed in this trivial K
specification, to serve as an example:

module TEMP

configuration <k> checkSat(
notBool (
        (exists
                (SetItem(#symInt(String2Id("s_elems_value")))
                        SetItem(#symInt(String2Id("s_elems_next_value")))
                        SetItem(#symInt(String2Id("x")))
                )
                .
                ((#symInt(String2Id("node_71_value")) ==Int
#symInt(String2Id("s_elems_value")) orBool #symInt(String2Id("node_71_value"))
==Int #symInt(String2Id("s_elems_next_value")) )
                        andBool notBool #symInt(String2Id("s_elems_value"))
==Int #symInt(String2Id("x"))
                )
        )
        impliesBool
        (exists
                (SetItem(#symInt(String2Id("s_elems_value")))
                        SetItem(#symInt(String2Id("x")))
                )
                .
                (#symInt(String2Id("node_71_value")) ==Int
#symInt(String2Id("s_elems_value"))
                        andBool notBool #symInt(String2Id("s_elems_value"))
==Int #symInt(String2Id("x"))
                )
        )
)
) </k>

endmodule

Compiling with the symbolic backend of K 3.4 and executing it gives me the
"unknown" result that I advanced before:

$ kompile temp.k --backend symbolic
$ krun -cPC=true
<k>
    "unknown"
</k>
<path-condition>
    true
</path-condition>

Considering that the call to Z3 was expected to return "unsat", I built the
SMTLib expression as done by K's translation engine and obtained the following
script:

(set-logic AUFNIRA)
(declare-fun __var__node_71_value () Int)
(assert (not (=> (exists ( (__var__s_elems_next_value Int)
(__var__s_elems_value Int) (__var__x Int) ) (and (or (= __var__node_71_value
__var__s_elems_value) (= __var__node_71_value __var__s_elems_next_value)) (not
(= __var__s_elems_value __var__x )))) (exists ( (__var__s_elems_value Int)
(__var__x Int) ) (and (= __var__node_71_value __var__s_elems_value) (not (=
__var__s_elems_value __var__x)))))))
(check-sat)

Copy/pasting this script in the web application at "http://rise4fun.com/Z3";
and executing it gave me as a result the "unsat" that I was looking for.

What can I do to solve this situation? Is there any way to change the solver
called to a external one (like CVC3), or a different version? (K 3.4 might be
running an outdated version of Z3). I tried changing the SMT solver with the
--smt option of krun, but nothing happened (even setting --smt to "none")...

Thanks in advance and sorry for the inconveniencies. This is important to me
since I am blocked in my research process unless I can solve this conflict...

Best regards,
Daniel