
Fix the following UCLID5 code using the compiler feedback provided below.

```

(set-logic ALL)

(declare-fun st () Int)
(declare-fun message1 () Bool)
(declare-fun message2 () Bool)
(declare-fun ack () Bool)

(define-fun property1 () Bool
    (=> (and (= st 0) message1) ack)
)

(define-fun property2 () Bool
    (=> (and (= st 1) message2) ack)
)

(define-fun property3 () Bool
    (=> (and (= ack true) (= st 0)) message2)
)

(define-fun property4 () Bool
    (=> (and (= ack true) (= st 1)) message1)
)

(assert (forall ((st Int) (message1 Bool) (message2 Bool) (ack Bool))
    (and (property1) (property2) (property3) (property4))
))

(check-sat)
```

Compiler feedback:

```
Syntax error on tmp.ucl, line 2: end of input expected.
(set-logic ALL)

```
Reply with your UCLID5 code inside one unique code block.

I can definitely do that! Here is the UCLID5 code:
```
