Unary negation on subrange type unsat initial state

[xaaronc]

With the following input:

type T = subrange [0,1] of int;
function A(x: T) returns (y: int)
let
	y = -x;
	--%PROPERTY y > 0;
tel

kind2 yields:

BMC Initial state is unsat, the system has no reachable states.
Property (y > 0) is valid by bounded model checking after 0.038s.

However if I use the binary negation: y = 0-x; then I get the expected result:

Property (y > 0) is invalid by property directed reachability for k=0 after 0.050s.

I would expect the expression y = -x; to either give a type error, or to yield the correct result (as in the 0-x case).

$ kind2 --version
kind2 v1.2.0-519-g8488b446

[daniel-larraz]

Thank you for reporting this bug. Pull request #671 fixes this issue