unknown for a very simple failing assertion

[chanheec]

After running Verus with the below example, Z3 gives unknown with (:reason-unknown "(incomplete quantifiers)"). I am wondering if this behavior is expected.

fn test_n(n: nat) {
    assert(n >= 5);      // FAILS
}

I expected to see sat for this example but I was a bit surprised to see unknown.
@jaybosamiya and I looked into the prelude a bit and found the prelude itself ends in unknown. There are several axioms that give unknown itself. For example, the first assert in the prelude also gives unknown.

;; ... 
;; set-option & declaration 
;; ...

(assert
 (=>
  fuel_defaults
  (forall ((id FuelId)) (!
    (= (fuel_bool id) (fuel_bool_default id))
    :pattern ((fuel_bool id))
))))
(check-sat)      ;; this gives unknown

[parno]

Here's the full SMT2 file:

(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.case_split 3)
(set-option :smt.qi.eager_threshold 100.0)
(set-option :smt.delay_units true)
(set-option :smt.arith.solver 2)
(set-option :smt.arith.nl false)

;; AIR prelude
(declare-sort FuelId 0)
(declare-fun fuel_bool (FuelId) Bool)
(declare-fun fuel_bool_default (FuelId) Bool)
(declare-const fuel_defaults Bool)

(assert
 (=>
  fuel_defaults
  (forall ((id FuelId)) (!
    (= (fuel_bool id) (fuel_bool_default id))
    :pattern ((fuel_bool id))
))))

;;(assert (not fuel_defaults))  ; Uncommenting this gives SAT
;;(assert fuel_defaults)        ; Uncommenting this instead still gives unknown
(check-sat)                     ; Produces unknown (and fails to create a model)

The fact that this produces unknown is troubling, since it seems, on the face of it, easy to produce sat -- just set fuel_defaults to false. Indeed, if we explicitly add that as an assertion (as shown in the comments), then we do get sat. However, if we explicitly set fuel_defaults to true via an assert, we still get unknown, even though here, one could presumably set (fuel_bool id) and (fuel_bool_default id) to different Boolean values.

For Verus debugger purposes, it's troubling that even the very simplest prefix of our prelude pushes us into unknown territory, which doesn't bode well for extracting sat models later on.

@Chris-Hawblitzel , @odedp: Do you have any insight into what might be happening here? Is it worth inquiring with the Z3 folks?

[Chris-Hawblitzel]

unknown is normal. I've only seen sat in the simplest examples, typically those with no quantifiers. If I try the following Verus example:

use builtin::*;

#[verifier(external)]
fn main() {
}

#[proof]
#[verifier(external_body)]
fn assert(b: bool) {
    requires(b);
    ensures(b);
}

fn test_n(n: nat) {
    assert(n >= 5);      // FAILS
}

I get this SMT file:

(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.case_split 3)
(set-option :smt.qi.eager_threshold 100.0)
(set-option :smt.delay_units true)
(set-option :smt.arith.solver 2)
(set-option :smt.arith.nl false)

;; Prelude

;; AIR prelude
(declare-sort %%Function%%)

(declare-sort FuelId 0)
(declare-sort Fuel 0)
(declare-const zero Fuel)
(declare-fun succ (Fuel) Fuel)
(declare-fun fuel_bool (FuelId) Bool)
(declare-fun fuel_bool_default (FuelId) Bool)
(declare-const fuel_defaults Bool)
(assert
 (=>
  fuel_defaults
  (forall ((id FuelId)) (!
    (= (fuel_bool id) (fuel_bool_default id))
    :pattern ((fuel_bool id))
))))
(declare-sort Poly 0)
(declare-fun I (Int) Poly)
(declare-fun B (Bool) Poly)
(declare-fun %I (Poly) Int)
(declare-fun %B (Poly) Bool)
(declare-sort Type 0)
(declare-const BOOL Type)
(declare-const INT Type)
(declare-const NAT Type)
(declare-fun UINT (Int) Type)
(declare-fun SINT (Int) Type)
(declare-fun has_type (Poly Type) Bool)
(declare-fun as_type (Poly Type) Poly)
(declare-fun mk_fun (%%Function%%) %%Function%%)
(assert
 (has_type (B true) BOOL)
)
(assert
 (has_type (B false) BOOL)
)
(assert
 (forall ((x Poly) (t Type)) (!
   (and
    (has_type (as_type x t) t)
    (=>
     (has_type x t)
     (= x (as_type x t))
   ))
   :pattern ((as_type x t))
)))
(assert
 (forall ((x %%Function%%)) (!
   (= (mk_fun x) x)
   :pattern ((mk_fun x))
)))
(assert
 (forall ((x Bool)) (!
   (= x (%B (B x)))
   :pattern ((B x))
)))
(assert
 (forall ((x Int)) (!
   (= x (%I (I x)))
   :pattern ((I x))
)))
(assert
 (forall ((x Poly)) (!
   (=>
    (has_type x BOOL)
    (= x (B (%B x)))
   )
   :pattern ((has_type x BOOL))
)))
(assert
 (forall ((x Poly)) (!
   (=>
    (has_type x INT)
    (= x (I (%I x)))
   )
   :pattern ((has_type x INT))
)))
(assert
 (forall ((x Poly)) (!
   (=>
    (has_type x NAT)
    (= x (I (%I x)))
   )
   :pattern ((has_type x NAT))
)))
(assert
 (forall ((bits Int) (x Poly)) (!
   (=>
    (has_type x (UINT bits))
    (= x (I (%I x)))
   )
   :pattern ((has_type x (UINT bits)))
)))
(assert
 (forall ((bits Int) (x Poly)) (!
   (=>
    (has_type x (SINT bits))
    (= x (I (%I x)))
   )
   :pattern ((has_type x (SINT bits)))
)))
(declare-const SZ Int)
(assert
 (or
  (= SZ 32)
  (= SZ 64)
))
(declare-fun uHi (Int) Int)
(declare-fun iLo (Int) Int)
(declare-fun iHi (Int) Int)
(assert
 (= (uHi 8) 256)
)
(assert
 (= (uHi 16) 65536)
)
(assert
 (= (uHi 32) 4294967296)
)
(assert
 (= (uHi 64) 18446744073709551616)
)
(assert
 (= (uHi 128) (+ 1 340282366920938463463374607431768211455))
)
(assert
 (= (iLo 8) (- 128))
)
(assert
 (= (iLo 16) (- 32768))
)
(assert
 (= (iLo 32) (- 2147483648))
)
(assert
 (= (iLo 64) (- 9223372036854775808))
)
(assert
 (= (iLo 128) (- 170141183460469231731687303715884105728))
)
(assert
 (= (iHi 8) 128)
)
(assert
 (= (iHi 16) 32768)
)
(assert
 (= (iHi 32) 2147483648)
)
(assert
 (= (iHi 64) 9223372036854775808)
)
(assert
 (= (iHi 128) 170141183460469231731687303715884105728)
)
(declare-fun nClip (Int) Int)
(declare-fun uClip (Int Int) Int)
(declare-fun iClip (Int Int) Int)
(assert
 (forall ((i Int)) (!
   (and
    (<= 0 (nClip i))
    (=>
     (<= 0 i)
     (= i (nClip i))
   ))
   :pattern ((nClip i))
)))
(assert
 (forall ((bits Int) (i Int)) (!
   (and
    (<= 0 (uClip bits i))
    (< (uClip bits i) (uHi bits))
    (=>
     (and
      (<= 0 i)
      (< i (uHi bits))
     )
     (= i (uClip bits i))
   ))
   :pattern ((uClip bits i))
)))
(assert
 (forall ((bits Int) (i Int)) (!
   (and
    (<= (iLo bits) (iClip bits i))
    (< (iClip bits i) (iHi bits))
    (=>
     (and
      (<= (iLo bits) i)
      (< i (iHi bits))
     )
     (= i (iClip bits i))
   ))
   :pattern ((iClip bits i))
)))
(declare-fun uInv (Int Int) Bool)
(declare-fun iInv (Int Int) Bool)
(assert
 (forall ((bits Int) (i Int)) (!
   (= (uInv bits i) (and
     (<= 0 i)
     (< i (uHi bits))
   ))
   :pattern ((uInv bits i))
)))
(assert
 (forall ((bits Int) (i Int)) (!
   (= (iInv bits i) (and
     (<= (iLo bits) i)
     (< i (iHi bits))
   ))
   :pattern ((iInv bits i))
)))
(assert
 (forall ((x Int)) (!
   (has_type (I x) INT)
   :pattern ((has_type (I x) INT))
)))
(assert
 (forall ((x Int)) (!
   (=>
    (<= 0 x)
    (has_type (I x) NAT)
   )
   :pattern ((has_type (I x) NAT))
)))
(assert
 (forall ((bits Int) (x Int)) (!
   (=>
    (uInv bits x)
    (has_type (I x) (UINT bits))
   )
   :pattern ((has_type (I x) (UINT bits)))
)))
(assert
 (forall ((bits Int) (x Int)) (!
   (=>
    (iInv bits x)
    (has_type (I x) (SINT bits))
   )
   :pattern ((has_type (I x) (SINT bits)))
)))
(assert
 (forall ((x Poly)) (!
   (=>
    (has_type x NAT)
    (<= 0 (%I x))
   )
   :pattern ((has_type x NAT))
)))
(assert
 (forall ((bits Int) (x Poly)) (!
   (=>
    (has_type x (UINT bits))
    (uInv bits (%I x))
   )
   :pattern ((has_type x (UINT bits)))
)))
(assert
 (forall ((bits Int) (x Poly)) (!
   (=>
    (has_type x (SINT bits))
    (iInv bits (%I x))
   )
   :pattern ((has_type x (SINT bits)))
)))
(declare-fun Mul (Int Int) Int)
(declare-fun EucDiv (Int Int) Int)
(declare-fun EucMod (Int Int) Int)
(assert
 (forall ((x Int) (y Int)) (!
   (= (Mul x y) (* x y))
   :pattern ((Mul x y))
)))
(assert
 (forall ((x Int) (y Int)) (!
   (= (EucDiv x y) (div x y))
   :pattern ((EucDiv x y))
)))
(assert
 (forall ((x Int) (y Int)) (!
   (= (EucMod x y) (mod x y))
   :pattern ((EucMod x y))
)))
(declare-fun check_decrease_int.? (Int Int Bool) Bool)
(assert
 (forall ((cur Int) (prev Int) (otherwise Bool)) (!
   (= (check_decrease_int.? cur prev otherwise) (or
     (and
      (<= 0 cur)
      (< cur prev)
     )
     (and
      (= cur prev)
      otherwise
   )))
   :pattern ((check_decrease_int.? cur prev otherwise))
)))
(declare-fun height.? (Poly) Int)
(assert
 (forall ((x Poly)) (!
   (<= 0 (height.? x))
   :pattern ((height.? x))
)))
(declare-fun uintxor (Int Poly Poly) Int)
(declare-fun uintand (Int Poly Poly) Int)
(declare-fun uintor (Int Poly Poly) Int)
(declare-fun uintshr (Int Poly Poly) Int)
(declare-fun uintshl (Int Poly Poly) Int)
(declare-fun uintnot (Int Poly) Int)

;; MODULE ''

;; Fuel
(assert
 true
)

;; Datatypes
(declare-datatypes ((tuple%0. 0)) (((tuple%0./tuple%0))))
(declare-const TYPE%tuple%0. Type)
(declare-fun Poly%tuple%0. (tuple%0.) Poly)
(declare-fun %Poly%tuple%0. (Poly) tuple%0.)
(assert
 (forall ((x@ tuple%0.)) (!
   (= x@ (%Poly%tuple%0. (Poly%tuple%0. x@)))
   :pattern ((Poly%tuple%0. x@))
)))
(assert
 (forall ((x@ Poly)) (!
   (=>
    (has_type x@ TYPE%tuple%0.)
    (= x@ (Poly%tuple%0. (%Poly%tuple%0. x@)))
   )
   :pattern ((has_type x@ TYPE%tuple%0.))
)))
(assert
 (forall ((x@ tuple%0.)) (!
   (has_type (Poly%tuple%0. x@) TYPE%tuple%0.)
   :pattern ((has_type (Poly%tuple%0. x@) TYPE%tuple%0.))
)))

;; Function-Specs crate::assert
(declare-fun req%assert. (Bool) Bool)
(declare-const %%global_location_label%%0 Bool)
(assert
 (forall ((b@ Bool)) (!
   (= (req%assert. b@) (=>
     %%global_location_label%%0
     b@
   ))
   :pattern ((req%assert. b@))
)))

;; Function-Axioms crate::assert
(declare-fun ens%assert. (Bool) Bool)
(assert
 (forall ((b@ Bool)) (!
   (= (ens%assert. b@) b@)
   :pattern ((ens%assert. b@))
)))

;; Function-Def crate::test_n
(push)
 (declare-const n@ Int)
 (declare-const tmp%1@ Bool)
 (assert
  fuel_defaults
 )
 (assert
  (<= 0 n@)
 )
 ;; precondition not satisfied
 (declare-const %%location_label%%0 Bool)
 (declare-const %%query%% Bool)
 (assert
  (=>
   %%query%%
   (not (=>
     (= tmp%1@ (>= n@ 5))
     (=>
      %%location_label%%0
      (req%assert. tmp%1@)
 )))))
 (assert
  %%query%%
 )
 (set-option :rlimit 30000000)
 (check-sat)
 (set-option :rlimit 0)
 (get-info :reason-unknown)
 (get-model)
 ;; ...
(pop)

;; ...

which generates:

unknown
(:reason-unknown "(incomplete quantifiers)")
(model
  ;; universe for Type:
  ;;   Type!val!0
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun Type!val!0 () Type)
  ;; cardinality constraint:
  (forall ((x Type)) (= x Type!val!0))
  ;; -----------
  ;; universe for Poly:
  ;;   Poly!val!0 Poly!val!1
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun Poly!val!0 () Poly)
  (declare-fun Poly!val!1 () Poly)
  ;; cardinality constraint:
  (forall ((x Poly)) (or (= x Poly!val!0) (= x Poly!val!1)))
  ;; -----------
  (define-fun n@ () Int
    0)
  (define-fun tmp%1@ () Bool
    false)
  (define-fun %%query%% () Bool
    true)
  (define-fun %%global_location_label%%0 () Bool
    true)
  (define-fun fuel_defaults () Bool
    true)
  (define-fun BOOL () Type
    Type!val!0)
  (define-fun SZ () Int
    32)
  (define-fun %%location_label%%0 () Bool
    true)
  (define-fun iHi ((x!0 Int)) Int
    (ite (= x!0 16) 32768
    (ite (= x!0 32) 2147483648
    (ite (= x!0 64) 9223372036854775808
    (ite (= x!0 128) 170141183460469231731687303715884105728
      128)))))
  (define-fun %B ((x!0 Poly)) Bool
    (ite (= x!0 Poly!val!1) false
      true))
  (define-fun iLo ((x!0 Int)) Int
    (ite (= x!0 16) (- 32768)
    (ite (= x!0 32) (- 2147483648)
    (ite (= x!0 64) (- 9223372036854775808)
    (ite (= x!0 128) (- 170141183460469231731687303715884105728)
      (- 128))))))
  (define-fun req%assert. ((x!0 Bool)) Bool
    false)
  (define-fun uHi ((x!0 Int)) Int
    (ite (= x!0 16) 65536
    (ite (= x!0 32) 4294967296
    (ite (= x!0 64) 18446744073709551616
    (ite (= x!0 128) 340282366920938463463374607431768211456
      256)))))
  (define-fun B ((x!0 Bool)) Poly
    (ite (= x!0 false) Poly!val!1
      Poly!val!0))
  (define-fun has_type ((x!0 Poly) (x!1 Type)) Bool
    true)
)

As far as I know, this is what's supposed to happen. Are you seeing something different?

[odedp]

For the file Bryan posted, if I just cut out all the configurations and run z3 on:

(declare-sort FuelId 0)
(declare-fun fuel_bool (FuelId) Bool)
(declare-fun fuel_bool_default (FuelId) Bool)
(declare-const fuel_defaults Bool)

(assert
 (=>
  fuel_defaults
  (forall ((id FuelId)) (!
    (= (fuel_bool id) (fuel_bool_default id))
    :pattern ((fuel_bool id))
))))

;;(assert (not fuel_defaults))  ; Uncommenting this gives SAT
;;(assert fuel_defaults)        ; Uncommenting this instead still gives unknown
(check-sat)                     ; Produces unknown (and fails to create a model)

Then I get SAT in < 1s. Same with cvc4 (even without flags).

unknown is normal. I've only seen sat in the simplest examples, typically those with no quantifiers.
...
As far as I know, this is what's supposed to happen. Are you seeing something different?

I think this may depend more on our specific choice of solver options than on the actual capabilities of solvers today. We got used to a mode of work where we never get models, and now we just configure z3 in a way that may improve the UNSAT performance at the expense of the SAT performance. I think it's pretty crazy that for Chris's example Verus says unknown instead of "you have an error, here's a counterexample". I think for such examples counterexamples are useful.

It may be that we want one solver configuration that is well-suited to the UNSAT case (like we have today) and another configuration (or another solver) that is well-suited to getting counterexamples and showing them to the user.

I'd like to put this on the stack for the "multi-solver" or "solver-manager" project, which I would say should just run both configs in parallel.

[Chris-Hawblitzel]

I'm still not sure I understand what the problem is. Z3 did generate a counterexample for the Verus code above. It says, for example: (define-fun n@ () Int 0), which gives n == 0 as a counterexample. We've also been using the generated models to print line number information in the errors. Since Z3 reliably generates models, do we need to care whether Z3 uses the term unknown instead of sat? Or do we have an example where Z3 fails to generate a model when it should?

[odedp]

What's the meaning of getting a model after an unknown result? Do we need to check ourselves if the model satisfies the constraints?

[Chris-Hawblitzel]

I think unknown just means that Z3 can't 100% guarantee that the formula is sat. For example, there might be a quantifier that could be instantiated to make the formula unsat, but Z3 could fail to instantiate the quantifier because its quantifier instantiation is incomplete, so it can't be sure that the formula really was sat.

[odedp]

But then what's the meaning of the model you get from (get-model)?

[odedp]

(I'm trying to get a sat result for the smt2 file @Chris-Hawblitzel shared, but so far no luck)

[odedp]

After some more experimentation I managed to get sat (both with z3 and cvc4) for the following file:

(set-logic UFDTNIA)

(declare-sort FuelId 0)
(declare-sort Fuel 0)
(declare-const zero Fuel)
(declare-fun succ (Fuel) Fuel)
(declare-fun fuel_bool (FuelId) Bool)
(declare-fun fuel_bool_default (FuelId) Bool)
(declare-const fuel_defaults Bool)
(assert
 (=>
  fuel_defaults
  (forall ((id FuelId)) (!
    (= (fuel_bool id) (fuel_bool_default id))
    :pattern ((fuel_bool id))
))))

;; Function-Specs crate::assert
(declare-fun req%assert. (Bool) Bool)
(declare-const %%global_location_label%%0 Bool)
(assert
 (forall ((b@ Bool)) (!
   (= (req%assert. b@) (=>
     %%global_location_label%%0
     b@
   ))
   :pattern ((req%assert. b@))
)))

;; Function-Def crate::test_n
 (declare-const n@ Int)
 (declare-const tmp%1@ Bool)
 (assert
  fuel_defaults
 )
 (assert
  (<= 0 n@)
 )
 ;; precondition not satisfied
 (declare-const %%location_label%%0 Bool)
 (declare-const %%query%% Bool)
 (assert
  (=>
   %%query%%
   (not (=>
     (= tmp%1@ (>= n@ 5))
     (=>
      %%location_label%%0
      (req%assert. tmp%1@)
 )))))
 (assert
  %%query%%
 )
(check-sat)
(get-model)

What I did was basically manually cutting out all the prelude and then putting things back only based on errors I got. I guess another thing a "solver-manager" can do is prune smt queries based on dependencies.

[Chris-Hawblitzel]

The model in the unknown case is the satisfying assignment to the variables that makes the formula true given the limited instantiations of quantifiers, limited results from nonlinear arithmetic, etc.

Just to reemphasize this: we expect Z3 to say unknown for verification failures. This is the way it's worked for Boogie, Dafny, and F* for many years. As long as Z3 generates the models, I don't see any need to try to get Z3 to say sat.

[parno]

In the tiny example file I posted (#158 (comment)), Z3 does fail to produce a model (unless you uncomment the line that produces sat). That example is also weird in that it feels like Z3 is overly eager to give up on finding SAT, just because a quantifier is mentioned.

I guess we can hope that in larger Verus examples, even when we get an unknown result, we'll still get a useful model out.

[Chris-Hawblitzel]

@parno The file you posted uses Z3 in a slightly different way than Verus/AIR/Dafny/Boogie/F*, because it never uses push and pop. Z3 configures itself differently in this case (although whether it's better or worse, or what it has to do with model generation, I don't know). You can see the difference if you ask for (get-info :reason-unknown). For this:

(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.case_split 3)
(set-option :smt.qi.eager_threshold 100.0)
(set-option :smt.delay_units true)
(set-option :smt.arith.solver 2)
(set-option :smt.arith.nl false)

;; AIR prelude
(declare-sort FuelId 0)
(declare-fun fuel_bool (FuelId) Bool)
(declare-fun fuel_bool_default (FuelId) Bool)
(declare-const fuel_defaults Bool)

(assert
 (=>
  fuel_defaults
  (forall ((id FuelId)) (!
    (= (fuel_bool id) (fuel_bool_default id))
    :pattern ((fuel_bool id))
))))

;;(assert (not fuel_defaults))  ; Uncommenting this gives SAT
;;(assert fuel_defaults)        ; Uncommenting this instead still gives unknown
(check-sat)                     ; Produces unknown (and fails to create a model)
(get-info :reason-unknown)
(get-model)

Z3 says:

unknown
(:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)")
(error "line 27 column 10: model is not available")

but with a push/pop, Z3 prints a slightly different message for reason-unknown and does print a model:

(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.case_split 3)
(set-option :smt.qi.eager_threshold 100.0)
(set-option :smt.delay_units true)
(set-option :smt.arith.solver 2)
(set-option :smt.arith.nl false)

;; AIR prelude
(declare-sort FuelId 0)
(declare-fun fuel_bool (FuelId) Bool)
(declare-fun fuel_bool_default (FuelId) Bool)
(declare-const fuel_defaults Bool)

(assert
 (=>
  fuel_defaults
  (forall ((id FuelId)) (!
    (= (fuel_bool id) (fuel_bool_default id))
    :pattern ((fuel_bool id))
))))

;;(assert (not fuel_defaults))  ; Uncommenting this gives SAT
;;(assert fuel_defaults)        ; Uncommenting this instead still gives unknown
(push)
(check-sat)                     ; Produces unknown (and fails to create a model)
(get-info :reason-unknown)
(get-model)
(pop)

output:

unknown
(:reason-unknown "(incomplete quantifiers)")
(
  (define-fun fuel_defaults () Bool
    false)
  (define-fun fuel_bool_default ((x!0 FuelId)) Bool
    false)
  (define-fun fuel_bool ((x!0 FuelId)) Bool
    false)
)
...

[parno]

Whoa, that's very interesting (and surprising)! Thanks for pointing out the difference.

[Chris-Hawblitzel]

There's some more information here: https://stackoverflow.com/questions/16422018/how-incremental-solving-works-in-z3

[Chris-Hawblitzel]

Also here: https://stackoverflow.com/questions/23736269/what-are-the-benefits-of-incremental-solving . "When push/pop commands are present, Z3 essentially switches to a completely different solver, because it detects that it needs support for incrementality. The incremental solver is usually (but not always) slower on non-incremental queries, but in turn can take advantage of incrementality."