Hello,

I get the following daily test results which all throw the same exception:

```
Prog2.tests.daily.VerificationTests::testEarlyReturnWhile2
java.lang.IllegalArgumentException: Expected the subformula TRUE to be of integer type.
at tinycc.logic.solver.z3.Z3Translator.translateIntSubformula(Z3Translator.java:154)
// more Z3 stuff
```

```
Prog2.tests.daily.VerificationTests::testEarlyReturnWhile
java.lang.IllegalArgumentException: Expected the subformula ((1 â 1) â TRUE) to be of integer type.
at tinycc.logic.solver.z3.Z3Translator.translateIntSubformula(Z3Translator.java:154)
// more Z3 stuff
```

```
Prog2.tests.daily.VerificationTests::testConstantConditional
java.lang.IllegalArgumentException: Expected the subformula ((0 == 0) â TRUE) to be of integer type.
at tinycc.logic.solver.z3.Z3Translator.translateIntSubformula(Z3Translator.java:154)
// more Z3 stuff
```

Since we do not implement `bool`

to `int`

conversion all of the formulas above should be of type `bool`

, yet the solver complains that they should be `int`

? I am a bit confused.

I also get this:

```
Prog2.tests.daily.TestsCorrect::all
java.lang.AssertionError: The following test cases fail on a correct implementation:
tinycc.tests.verification.VerificationTests.testLogicType(VerificationTests.java:58): IllegalArgumentException: Expected the subformula (Â¬(Â¬(0 â 0))) to be of integer type.
// testing stuff
```

which again should give `bool`

, not `int`

. Obviously this means my implementation is wrong, but why does it expect integers here? This test passes on my implementation.

The formula from my test is within an `_Assert`

statement:

```
1 == !!0
```

and while I can not make out the symbol between the two zeroes in the result it should be a \neq, i.e the sub formula should be \neg (\neg (0 \neq 0)), which must have type `bool`

.

(Yes, I realize that this formula is within an `_Assert`

statement in a positive test.)