I'm in the process of verifying properties about equations written in a synchronous programming language, by compiling said language to Z3, using the PDR engine. I use Z3 4.5.1 compiled from Github's master branch a week ago.
For your curiosity's sake, I use a derivative of the translation from the synchronous language Lustre to Z3 proposed in this paper (but it's not necessary to read it to understand what I want to do).
I have a problem with the following program, that returns sat while I think it should return unsat:
(declare-var out Int)
(declare-var next_out Int)
(declare-var mem Int)
(declare-var next_mem Int)
(declare-var ok Bool)
(declare-var next_ok Bool)
(declare-rel Init (Int Int Bool))
(declare-rel Trans (Int Int Bool Int Int Bool))
(declare-rel Main (Int Int Bool))
(declare-rel Error ())
(rule (=> (= mem 0) (Init out mem ok)))
(rule (=> (and (= next_ok (>= next_out 0))
(= next_mem (+ mem 1))
(= next_out mem))
(Trans out mem ok next_out next_mem next_ok)))
(rule (=> (and (Init out mem ok)
(Trans out mem ok next_out next_mem next_ok))
(Main next_out next_mem next_ok)))
(rule (=> (and (Trans out mem ok next_out next_mem next_ok)
(Main out mem ok))
(Main next_out next_mem next_ok)))
(rule (=> (and (Main out mem ok)
(not ok))
Error))
(query Error :print-certificate true)
I'll try and simplify what's my intention so you don't have to go through the paper. We define three sequences mem, out and ok so that:
forall n > 0. mem(n) = mem(n - 1) + 1 with mem(0) = 0
and out(n) = mem(n - 1)
and ok(n) = out(n) >= 0
We want to prove that forall n > 0. ok(n) = true.
In the Z3 program, you can think of mem, out and ok as the values of the sequences at n - 1 (or the memories containing the previous values of the sequences) and next_* as the values at n.
The Init relation states that the initial equations are correct (that is the equations for n = 0), in our case we just have mem = 0 while out and ok are left free (that's rule 1). The Trans relation establishes that the relation between the n-th values and the n - 1-th values is correct (that's rule 2).
The Main relation states that, for a certain n > 0, the values of the sequences are coherent with the equations given (I'm not sure that's the best way of explaining it, if it's unclear please tell me). Thus rule 3 states that if the relations between the memories at n = 0 and the relation between these memories and the new values at n = 1 are correct, then we get a coherent set of values for n = 1. Rule 4 states that if we have a coherent set of sequence value at n, and that the relation between them and the values at n + 1 is correct, then we get a new coherent set of sequence values at n + 1.
The last rule is the property we want to check: given a coherent set of values, we cannot have that ok is false.
When I run this, I get:
sat
(and (Main!slice!1 false) (not (>= (:var 5) 0)) (Main!slice!1 true))
and I can't understand why. Am I missing something?
EDIT
I continued to work on the problem, trying to understand what Z3 was doing with what I gave him.
I ran it with the option fixedpoint.xform.inline_eager=false which (I suppose) makes it inline less. When running with verbosity level 1, I saw that after the first application of N7datalog15mk_rule_inlinerE I had 5 rules instead of 3 (see below for the full output). I also had the following result :
unsat
(define-fun I ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
(>= x!1 0))
(define-fun T ((x!0 Int) (x!1 Int) (x!2 Bool) (x!3 Int) (x!4 Int) (x!5 Bool)) Bool
(and (<= (+ x!1 (* (- 1) x!4)) (- 1)) (= x!5 (>= x!1 0))))
(define-fun M ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
(and x!2 (>= x!1 1)))
which is quite different from the original one… So unless I'm wrong about what the option above does, I guess it's a bug so I'll open an issue.
Full output
Running with z3 <file> -smt2 -v:1:
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...6 rules 0s)
(transform N7datalog27mk_quantifier_instantiationE...no-op 0s)
(transform N7datalog8mk_scaleE...no-op 0s)
(transform N7datalog18mk_karr_invariantsE...no-op 0s)
(transform N7datalog14mk_array_blastE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog12mk_bit_blastE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...3 rules 0s)
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...3 rules 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...3 rules 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog8mk_sliceE...3 rules 0s)
Entering level 1
Entering level 2
2 query!0 closed
true 1
1 Main!slice!1 closed
(not Main!slice!1_0_n) 182
0 Main!slice!1 closed
true 1
goals 0
sat
(and (Main!slice!1 false) (not (>= (:var 5) 0)) (Main!slice!1 true))
Running with z3 <file> -smt2 -v:1 fixedpoint.xform.inline_eager=false:
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...6 rules 0s)
(transform N7datalog27mk_quantifier_instantiationE...no-op 0s)
(transform N7datalog8mk_scaleE...no-op 0s)
(transform N7datalog18mk_karr_invariantsE...no-op 0s)
(transform N7datalog14mk_array_blastE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog12mk_bit_blastE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...5 rules 0s)
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...5 rules 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...5 rules 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog8mk_sliceE...no-op 0s)
Entering level 1
Entering level 2
Entering level 3
(define-fun Init ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
(>= x!1 0))
(define-fun Main ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
(and (>= x!1 1) x!2))
(define-fun Trans ((x!0 Int)
(x!1 Int)
(x!2 Bool)
(x!3 Int)
(x!4 Int)
(x!5 Bool)) Bool
(and (<= (+ x!1 (* (- 1) x!4)) (- 1)) (= x!5 (>= x!1 0))))
unsat
(define-fun Init ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
(>= x!1 0))
(define-fun Main ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
(and x!2 (>= x!1 1)))
(define-fun Trans ((x!0 Int)
(x!1 Int)
(x!2 Bool)
(x!3 Int)
(x!4 Int)
(x!5 Bool)) Bool
(and (<= (+ x!1 (* (- 1) x!4)) (- 1)) (= x!5 (>= x!1 0))))
This behaviour was due to a bug that has now been fixed. The discussion here contains the commit correcting it.