z3 behavior depends on the names of the functions

[mikulas-patocka]

Hi

I was verifying the same program with the same z3 version on two machines - and on one machine the verification passed and on the other machine z3 blew up memory in an infinite loop.

I analyzed the problem and it turned out that it was caused by the fact that the program was located in different directories. The verifier mangles the directory path into function names in the z3 script - and z3 behaves differently depending on the function names even if the rest of the script is otherwise identical.

This difference in behavior only happens when using the z3 library. It doesn't happen when processing the script with the z3 binary.

How to reproduce:

Use current z3 from git (339f0cd).
Compile this program with "gcc z3.c -lz3"

#include <stdio.h>
#include <z3.h>

char buffer[1 << 20];

int main(void)
{
        Z3_context z3;
        size_t n;
        const char *r;
        int code;
        z3 = Z3_mk_context(NULL);
        n = fread(buffer, 1, sizeof buffer, stdin);
        r = Z3_eval_smtlib2_string(z3, buffer);
        code = Z3_get_error_code(z3);
        printf("result: %s %d\n", r, code);
        return 0;
}

Download these two files:
z3-unsat.txt
z3-oom.txt

Run:
./a.out <z3-unsat.txt
You get unsat
./a.out <z3-oom.txt
Allocates memory in a loop until killed by the oom killer

[mikulas-patocka]

So, I fixed the infinite loop with this commit:
mikulas-patocka/ajla@bd4ba66

I added "assume marked >= 0" and the verification passes on both machines, which means that z3 couldn't infer that the value is positive. The "marked" variable is modified using the bit-complement operator (btc) - see "(define-fun int-btc" in the script.

So, the problem is that - depending on function names - z3 sees or doesn't see that a positive value with a toggled bit is still positive. Do you seed the pseudorandom number generator with the function names? Or, is there some read of uninitialized memory?

[mikulas-patocka]

So, I tried to force this claim as an axiom with:
(assert (forall ((x Int) (y Int) (z Int)) (! (= (< x 0) (< (int-btc x y z) 0)) :pattern ((int-btc x y z)))))

And I got warning "'if' cannot be used in patterns"

When I changed the definition of int-btc from "define-fun" to "define-fun-rec", the warning disappeared. Is it a proper way to deal with the warning?

(BTW. the warning processing is not thread-safe, I got crashes in warning_msg when running libz3 multithreaded and multiple threads were simultaneously generating the warning)