How to model variable swap in SMT (Z3)?

Question

I have a program that sorts variables, and I'm trying to check its validity with Z3, but I have one code segment where the variables are being swapped and I don't know how to model it in SMT syntax. Here is the original code segment:

if (x > y) {
  temp = x;
  x = y;
  y = temp;
}

And regarding the SMT I have written an assertion, but I guess it is not exactly the correct thing:

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun temp () Int)

(assert (=> (> s1 s2) (and (= tmp s1) (= s1 s2) (= s2 tmp))))

Any ideas how to do variable assignment in SMT?

Answer 1

You should look into Single Static Assignment [1]. In this way you can rewrite your original code as follows.

if (x0 > y0) {
  temp0 = x0;
  x1 = y0;
  y1 = temp0;
}

It thus becomes clear that you have two different instances of x and y. The first (x0, y0) is the one you are comparing in the if condition. The second (x1, y1) is the result of the operation.

This introduces an implicit notion of time that makes it also easier to write properties about your code. E.g.,

  ((x1 = x0) & (y1 = y0)) | ((x1 = y0) | (y1 = x0))

Of course, this might require adjusting other parts of your code, so that you are using the right variables.

[1] https://en.wikipedia.org/wiki/Static_single_assignment_form