PROOF_MODE affects outcome of check

1
votes

We are trying to use z3 to generate proofs, through the C API (through ScalaZ3). we thus enable the proof generation by setting PROOF=true. This however affects the result of other checks. Note that we do not use tactics/goals, we simply create a new solver and assert constraints and check.

For instance, on the following constraint (where x is of sort Integer):

(x + x) != (2 * x)

check() returns UNSAT with PROOF=false as expected. With PROOF=true however, it returns SAT with model (x -> 1).

We do not specify any logic in particular. We tried explicitly requesting a solver over QF_AUFLIA, but it's unclear whether the logic is silently ignored/unknown, or if it has no effect on this issue. It looks as if + becomes uninterpreted when proofs-production is requested.

Are we missing something obvious with this proof_generation mode?

EDIT 2:

We are using latest unstable from git (5b5a474b5443) in debug mode.

Here is the trace we get with PROOF=true:

R
C 3
= 0x7f04a0091a08
R
P 0x7f04a0091a08
S "MODEL"
S "true"
C 5
R
P 0x7f04a0091a08
S "TYPE_CHECK"
S "true"
C 5
R
P 0x7f04a0091a08
S "PROOF"
S "true"
C 5
R
P 0x7f04a0091a08
S "WELL_SORTED_CHECK"
S "true"
C 5
R
I 1
C 273
R
P 0x7f04a0091a08
C 7
= 0x7f04a00abda8
R
P 0x7f04a00abda8
C 33
= 0x7f04a00915e8
R
P 0x7f04a00abda8
P 0x7f04a00915e8
C 9
R
P 0x7f04a00abda8
C 32
= 0x7f04a007a2c8
R
P 0x7f04a00abda8
P 0x7f04a007a2c8
C 9
R
P 0x7f04a00abda8
S "Unit"
C 30
R
P 0x7f04a00abda8
S "Unit"
C 30
R
P 0x7f04a00abda8
S "isUnit"
C 30
R
P 0x7f04a00abda8
$ |Unit|
$ |isUnit|
U 0
s 0
p 0
u 0
C 41
= 0x7f04a00ab4c8
R
P 0x7f04a00abda8
U 1
P 0x7f04a00ab4c8
p 1
C 44
= 0x7f04a006c218
R
P 0x7f04a00abda8
U 1
$ |Unit|
s 1
P 0
p 1
P 0x7f04a006c218
p 1
C 46
@ 0x7f04a00ab1c8 3 0
@ 0x7f04a006c218 4 0
R
P 0x7f04a00abda8
P 0x7f04a006c218
C 45
R
P 0x7f04a00abda8
P 0x7f04a00ab4c8
U 0
P 0
P 0
p 0
C 47
* 0x7f04a00ab2f8 3
* 0x7f04a00ab0f8 4
R
P 0x7f04a00abda8
P 0x7f04a00ab2f8
C 9
R
P 0x7f04a00abda8
P 0x7f04a00ab0f8
C 9
R
P 0x7f04a00abda8
P 0x7f04a00ab1c8
C 9
R
P 0x7f04a00abda8
P 0x7f04a00ab2f8
U 0
p 0
C 49
= 0x7f04a006ab98
R
P 0x7f04a00abda8
P 0x7f04a006ab98
C 9
R
P 0x7f04a00abda8
C 32
= 0x7f04a007a2c8
R
P 0x7f04a00abda8
P 0x7f04a00915e8
P 0x7f04a007a2c8
C 37
= 0x7f04a00ab538
R
P 0x7f04a00abda8
P 0x7f04a00ab538
C 9
R
P 0x7f04a00abda8
S "card"
U 1
P 0x7f04a00ab538
p 1
P 0x7f04a00915e8
C 51
= 0x7f04a007a588
R
P 0x7f04a00abda8
P 0x7f04a007a588
C 9
R
P 0x7f04a00abda8
S "setMin"
U 1
P 0x7f04a00ab538
p 1
P 0x7f04a00915e8
C 51
= 0x7f04a00ab3e8
R
P 0x7f04a00abda8
P 0x7f04a00ab3e8
C 9
R
P 0x7f04a00abda8
S "setMax"
U 1
P 0x7f04a00ab538
p 1
P 0x7f04a00915e8
C 51
= 0x7f04a00ab068
R
P 0x7f04a00abda8
P 0x7f04a00ab068
C 9
R
P 0x7f04a00abda8
U 0
s 0
p 0
p 0
C 46
R
P 0x7f04a00abda8
S "QF_AUFLIA"
C 30
R
P 0x7f04a00abda8
$ |QF_AUFLIA|
C 412
= 0x7f04a00bfb38
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
C 417
R
P 0x7f04a00abda8
S "start0"
P 0x7f04a007a2c8
C 52
= 0x7f04a00bfc38
R
P 0x7f04a00abda8
P 0x7f04a00bfc38
C 9
R
P 0x7f04a00abda8
S "x0"
P 0x7f04a00915e8
C 52
= 0x7f04a00a55a8
R
P 0x7f04a00abda8
P 0x7f04a00a55a8
C 9
R
P 0x7f04a00abda8
U 2
P 0x7f04a00a55a8
P 0x7f04a00a55a8
p 2
C 64
= 0x7f04a00a51a8
R
P 0x7f04a00abda8
P 0x7f04a00a51a8
C 9
R
P 0x7f04a00abda8
I 2
P 0x7f04a00915e8
C 145
= 0x7f04a00a5528
R
P 0x7f04a00abda8
P 0x7f04a00a5528
C 9
R
P 0x7f04a00abda8
U 2
P 0x7f04a00a5528
P 0x7f04a00a55a8
p 2
C 65
= 0x7f04a00bf478
R
P 0x7f04a00abda8
P 0x7f04a00bf478
C 9
R
P 0x7f04a00abda8
U 2
P 0x7f04a00a51a8
P 0x7f04a00bf478
p 2
C 56
= 0x7f04a00bfd48
R
P 0x7f04a00abda8
P 0x7f04a00bfd48
C 9
R
P 0x7f04a00abda8
P 0x7f04a00bfc38
P 0x7f04a00bfd48
C 60
= 0x7f04a00bfda8
R
P 0x7f04a00abda8
P 0x7f04a00bfda8
C 9
R
P 0x7f04a00abda8
S "x0"
P 0x7f04a00915e8
C 52
= 0x7f04a00a50d8
R
P 0x7f04a00abda8
P 0x7f04a00a50d8
C 9
R
P 0x7f04a00abda8
P 0x7f04a00bfda8
U 2
P 0x7f04a00a55a8
P 0x7f04a00bfc38
p 2
P 0x7f04a00a50d8
P 0x7f04a00bfc38
p 2
C 245
= 0x7f04a00018d8
R
P 0x7f04a00abda8
P 0x7f04a00018d8
C 9
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
P 0x7f04a00bfc38
C 423
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
P 0x7f04a00018d8
C 423
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
C 419
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
U 0
p 0
C 427
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
U 1
C 420
R
P 0x7f04a00abda8
P 0x7f04a00bfb38
C 428
= 0x7f04a011a9e8
R
P 0x7f04a00abda8
P 0x7f04a011a9e8
C 248
R
P 0x7f04a00abda8
P 0x7f04a011a9e8
P 0x7f04a00a50d8
I 0
P 0
C 250
* 0x7f04a00ff678 4
R
P 0x7f04a00abda8
P 0x7f04a00ff678
C 9
R
P 0x7f04a00abda8
P 0x7f04a00ff678
I 0
C 219

Here is the trace we get with PROOF=false:

R
C 3
= 0x7f489c03aef8
R
P 0x7f489c03aef8
S "MODEL"
S "true"
C 5
R
P 0x7f489c03aef8
S "TYPE_CHECK"
S "true"
C 5
R
P 0x7f489c03aef8
S "PROOF"
S "false"
C 5
R
P 0x7f489c03aef8
S "WELL_SORTED_CHECK"
S "true"
C 5
R
I 1
C 273
R
P 0x7f489c03aef8
C 7
= 0x7f489c06fe48
R
P 0x7f489c06fe48
C 33
= 0x7f489c0acba8
R
P 0x7f489c06fe48
P 0x7f489c0acba8
C 9
R
P 0x7f489c06fe48
C 32
= 0x7f489c0112a8
R
P 0x7f489c06fe48
P 0x7f489c0112a8
C 9
R
P 0x7f489c06fe48
S "Unit"
C 30
R
P 0x7f489c06fe48
S "Unit"
C 30
R
P 0x7f489c06fe48
S "isUnit"
C 30
R
P 0x7f489c06fe48
$ |Unit|
$ |isUnit|
U 0
s 0
p 0
u 0
C 41
= 0x7f489c0ccff8
R
P 0x7f489c06fe48
U 1
P 0x7f489c0ccff8
p 1
C 44
= 0x7f489c010c38
R
P 0x7f489c06fe48
U 1
$ |Unit|
s 1
P 0
p 1
P 0x7f489c010c38
p 1
C 46
@ 0x7f489c0ae2f8 3 0
@ 0x7f489c010c38 4 0
R
P 0x7f489c06fe48
P 0x7f489c010c38
C 45
R
P 0x7f489c06fe48
P 0x7f489c0ccff8
U 0
P 0
P 0
p 0
C 47
* 0x7f489c0c3ae8 3
* 0x7f489c0736e8 4
R
P 0x7f489c06fe48
P 0x7f489c0c3ae8
C 9
R
P 0x7f489c06fe48
P 0x7f489c0736e8
C 9
R
P 0x7f489c06fe48
P 0x7f489c0ae2f8
C 9
R
P 0x7f489c06fe48
P 0x7f489c0c3ae8
U 0
p 0
C 49
= 0x7f489c0be318
R
P 0x7f489c06fe48
P 0x7f489c0be318
C 9
R
P 0x7f489c06fe48
C 32
= 0x7f489c0112a8
R
P 0x7f489c06fe48
P 0x7f489c0acba8
P 0x7f489c0112a8
C 37
= 0x7f489c0b5c18
R
P 0x7f489c06fe48
P 0x7f489c0b5c18
C 9
R
P 0x7f489c06fe48
S "card"
U 1
P 0x7f489c0b5c18
p 1
P 0x7f489c0acba8
C 51
= 0x7f489c0739f8
R
P 0x7f489c06fe48
P 0x7f489c0739f8
C 9
R
P 0x7f489c06fe48
S "setMin"
U 1
P 0x7f489c0b5c18
p 1
P 0x7f489c0acba8
C 51
= 0x7f489c0cc1a8
R
P 0x7f489c06fe48
P 0x7f489c0cc1a8
C 9
R
P 0x7f489c06fe48
S "setMax"
U 1
P 0x7f489c0b5c18
p 1
P 0x7f489c0acba8
C 51
= 0x7f489c073768
R
P 0x7f489c06fe48
P 0x7f489c073768
C 9
R
P 0x7f489c06fe48
U 0
s 0
p 0
p 0
C 46
R
P 0x7f489c06fe48
S "QF_AUFLIA"
C 30
R
P 0x7f489c06fe48
$ |QF_AUFLIA|
C 412
= 0x7f489c0714f8
R
P 0x7f489c06fe48
P 0x7f489c0714f8
C 417
R
P 0x7f489c06fe48
S "start0"
P 0x7f489c0112a8
C 52
= 0x7f489c0d5488
R
P 0x7f489c06fe48
P 0x7f489c0d5488
C 9
R
P 0x7f489c06fe48
S "x0"
P 0x7f489c0acba8
C 52
= 0x7f489c0c37d8
R
P 0x7f489c06fe48
P 0x7f489c0c37d8
C 9
R
P 0x7f489c06fe48
U 2
P 0x7f489c0c37d8
P 0x7f489c0c37d8
p 2
C 64
= 0x7f489c0d07b8
R
P 0x7f489c06fe48
P 0x7f489c0d07b8
C 9
R
P 0x7f489c06fe48
I 2
P 0x7f489c0acba8
C 145
= 0x7f489c0cca98
R
P 0x7f489c06fe48
P 0x7f489c0cca98
C 9
R
P 0x7f489c06fe48
U 2
P 0x7f489c0cca98
P 0x7f489c0c37d8
p 2
C 65
= 0x7f489c0b0c08
R
P 0x7f489c06fe48
P 0x7f489c0b0c08
C 9
R
P 0x7f489c06fe48
U 2
P 0x7f489c0d07b8
P 0x7f489c0b0c08
p 2
C 56
= 0x7f489c0cbb78
R
P 0x7f489c06fe48
P 0x7f489c0cbb78
C 9
R
P 0x7f489c06fe48
P 0x7f489c0d5488
P 0x7f489c0cbb78
C 60
= 0x7f489c0cbbd8
R
P 0x7f489c06fe48
P 0x7f489c0cbbd8
C 9
R
P 0x7f489c06fe48
S "x0"
P 0x7f489c0acba8
C 52
= 0x7f489c181a78
R
P 0x7f489c06fe48
P 0x7f489c181a78
C 9
R
P 0x7f489c06fe48
P 0x7f489c0cbbd8
U 2
P 0x7f489c0c37d8
P 0x7f489c0d5488
p 2
P 0x7f489c181a78
P 0x7f489c0d5488
p 2
C 245
= 0x7f489c181a28
R
P 0x7f489c06fe48
P 0x7f489c181a28
C 9
R
P 0x7f489c06fe48
P 0x7f489c0714f8
P 0x7f489c0d5488
C 423
R
P 0x7f489c06fe48
P 0x7f489c0714f8
P 0x7f489c181a28
C 423
R
P 0x7f489c06fe48
P 0x7f489c0714f8
C 419
R
P 0x7f489c06fe48
P 0x7f489c0714f8
U 0
p 0
C 427
R
P 0x7f489c06fe48
P 0x7f489c0714f8
U 1
C 420
R
P 0x7f489c06fe48
P 0x7f489c0714f8
C 430
= 0x7f489c0cc9f8
R
P 0x7f489c06fe48
P 0x7f489c0cc9f8
C 330
R
P 0x7f489c06fe48
P 0x7f489c0cc9f8
C 332

EDIT 3:

I created a small C program that reproduces the issue:

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

int main(int argc, char **args) {
    Z3_open_log("z3.log");

    int proofMode = (argc > 1);

    Z3_config conf = Z3_mk_config();

    Z3_set_param_value(conf, "MODEL", "true");
    Z3_set_param_value(conf, "TYPE_CHECK", "true");
    Z3_set_param_value(conf, "WELL_SORTED_CHECK", "true");

    if (proofMode) {
        Z3_set_param_value(conf, "PROOF", "true");
    } else {
        Z3_set_param_value(conf, "PROOF", "false");
    }

    Z3_context ctx   = Z3_mk_context_rc(conf);

    Z3_solver solver = Z3_mk_solver(ctx);

    Z3_sort boolSort = Z3_mk_bool_sort(ctx);
    Z3_sort intSort  = Z3_mk_int_sort(ctx);

    Z3_ast x     = Z3_mk_fresh_const(ctx, "x", intSort);
    Z3_inc_ref(ctx, x);

    Z3_ast newX  = Z3_mk_fresh_const(ctx, "x", intSort);
    Z3_inc_ref(ctx, newX);

    Z3_ast c2    = Z3_mk_int(ctx, 2, intSort);
    Z3_inc_ref(ctx, c2);

    Z3_ast start = Z3_mk_fresh_const(ctx, "start", boolSort);
    Z3_inc_ref(ctx, start);

    Z3_ast xpx_args[2] = {x, x};
    Z3_ast xpx         = Z3_mk_add(ctx, 2, xpx_args);
    Z3_inc_ref(ctx, xpx);

    Z3_ast xt2_args[2] = {c2, x};
    Z3_ast xt2         = Z3_mk_mul(ctx, 2, xt2_args);
    Z3_inc_ref(ctx, xt2);

    Z3_ast dis_args[2] = {xpx, xt2};
    Z3_ast dis         = Z3_mk_distinct(ctx, 2, dis_args);
    Z3_inc_ref(ctx, dis);

    Z3_ast res = Z3_mk_implies(ctx, start, dis);
    Z3_inc_ref(ctx, res);

    printf("AST Before: %s\n", Z3_ast_to_string(ctx, res));

    // Substituting
    Z3_ast substRes = Z3_substitute(ctx, res, 1, &x, &newX);
    Z3_inc_ref(ctx, substRes);

    printf("AST After: %s\n", Z3_ast_to_string(ctx, substRes));

    // Solving
    Z3_solver_assert(ctx, solver, start);
    Z3_solver_assert(ctx, solver, substRes);

    Z3_lbool solverRes = Z3_solver_check(ctx, solver);

    printf("Solver (proofMode=%s) returned %s\n", proofMode ? "true" : "false", (solverRes == Z3_L_FALSE ? "UNSAT" : (solverRes == Z3_L_TRUE ? "SAT" : "UNKNOWN")));

    return 0;
}

With the following Makefile:

all: compile runproof runnoproof

compile:
    gcc -o test -I../z3/src/api/ -L ../z3/build/ -lz3 -g -fPIC -O2 -fopenmp test.c

runproof: compile
    LD_LIBRARY_PATH="../z3/build/" ./test proof

runnoproof: compile
    LD_LIBRARY_PATH="../z3/build/" ./test

I get the following results against latest z3 unstable:

$ make
gcc -o test -I../z3/src/api/ -L ../z3/build/ -lz3 -g -fPIC -O2 -fopenmp test.c

LD_LIBRARY_PATH="../z3/build/" ./test proof
AST Before: (=> start!2 (distinct (+ x!0 x!0) (* 2 x!0)))
AST After: (or (not start!2) (not (= (* 2 x!1) (* 2 x!0))))
Solver (proofMode=true) returned SAT

LD_LIBRARY_PATH="../z3/build/" ./test
AST Before: (=> start!2 (distinct (+ x!0 x!0) (* 2 x!0)))
AST After: (not start!2)
Solver (proofMode=false) returned UNSAT
1
z3
Which version are you using? Could you create a log of the execution trace? This link explains how to do it: stackoverflow.com/questions/14821687/encoding-returns-unknown/… – Leonardo de Moura
@leonardo I have updated the question accordingly! – Etienne Kneuss
The trace above was not generated with the "unstable" branch (hash ecceb0accc). This is a trace from an older version of Z3. Could you check if you are linking with the correct version? – Leonardo de Moura
Doh, indeed, sorry. PROOF_MODE is not even available as a config parameter anymore: Is the only way to enable proof generation now to use goals? – Etienne Kneuss
We have a new parameter setting framework. The parameters are organized in modules. PROOF_MODE is now called PROOF and it is a Boolean parameter. We can execute z3 -p to list all parameters. We can also get a more detailed description using z3 -pd. – Leonardo de Moura

1 Answers

0
votes

The formulas sent to the solver object are different in the two different logs. In the first log, the following formulas are asserted:

  start0!3
  (or (not start0!3) (not (= (* 2 x0!5) (* 2 x0!4))))

Z3 correctly reports sat. In the second log, the following formulas are asserted:

  start0!3
  (not start0!3)

Could you check if the logs were correctly generated? You can also trace your own asserts by printing them before each "assert" call. I also executed the logs using Valgrind, and no memory corruption was detected.