Solver reports type error during verification

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.)

The error you get seems to occur when the left subformula in an operation has type INT, but the right one has type BOOL.
Note that this happens before the operation is checked, so the actual cause could be a formula of type INT in an AND or similar!

So you should probably check whether this can happen with your code.

In particular, Expressions are not the only places where you might have to perform conversions from INT to BOOL.

For example, 1 is also a valid condition and a valid invariant.

1 Like

is the expression (x) also a valid invariant?

is the expression (x) also a valid invariant?

Syntactically, yes. It’s equivalent to x ≠ 0.
Of course, whether this is actually a valid invariant depends on the loop body.

2 Likes

yes sure, Syntactically is what I meant.

@Bastian.Heinen
For your own test:

The expression 1 == !!0 is a problem, as the reference does not convert the left side to boolean here.

Why?
Well, while it would work in this specific case, you would have a problem in general. Since C does not have booleans, the result of ! is a number, and C would do an integer comparison here.

However, consider the expression 2 == !x. In C, this would never be true, as !x is 0 or 1, but never 2.
But for our formulas, the right hand side has type BOOL, so you would convert the left hand side to BOOL as well - and suddenly, the formula can be true.

Obviously, this is an issue, as now our verifier no longer matches the behaviour of the program.

I think that we just ignore this issue for this project, so this case is not tested. You can do the conversion in your implementation if you want, but the reference does not, so you might want to change your test to not use it.

1 Like

Well, now I feel stupid. Of course those need to be translated as well. :grinning: Thanks!