Garbage SMT queries

[catalin-hritcu]

When looking with Simon at the output of Z3 on a file obtained with --logQueries on tinyfstar-new.fst, we first observed that there are a lot of model is not available errors. Maybe those are expected(?) so we filtered those out and then we found this:

(error "line 208792 column 14: unknown constant @x3")
(error "line 208889 column 14: unknown constant @x3")
(error "line 209035 column 0: unknown constant @x4")
(error "line 209180 column 0: unknown constant @x4")
unknown

The code in question looks like this:

;;;;;;;;;;;;;;;;Exp_abs_7904 typing
(assert (forall ((@x0 Term) (@x1 Term) (@x2 Term))
 (! (HasType (Exp_abs_7904 @x0
@x1
@x2)
(Typ_fun_7906 @x3
@x4
@x2
@x2))

(and something very similar for the other 3 errors)
The variables in question are really not bound. Is this reasonable? Is it normal to ignore SMT queries that return errors? I'm a bit worried about "garbage in, garbage out" behavior.

Just for the record, saving the invocation we used for calling z3 from the command line:

z3 -smt2 -t:10 AUTO_CONFIG=false MODEL=true SMT.RELEVANCY=2 queries-bg-2.smt2 | grep -v "model is not available"

[nikswamy]

Fyi, minimized a related example to the one below.

Repro with

$ fstar --universes --explicit_deps test.fst --log_queries
$ z3 queries-bg-0.smt2 | grep error | grep -v model

module Test
assume type grows : nat -> nat -> Type0
let reln (a:Type) = a -> a -> Type

assume type m_rref : a:Type -> reln a -> Type0
assume val m_contains : a:Type -> b:reln a -> r:m_rref a b -> GTot bool

let genPost (log:m_rref nat grows) h1 = 
    m_contains nat grows log

UPDATE: FIXED NOW

[vkanne-msft]

We should hard fail on SMT errors.

[nikswamy]

strange. it was not my intention to close it. GitHub did it automatically ...

[msprotz]

"fix #N" and "fixes #N" in the commit message have the side-effect of closing the corresponding bug

[catalin-hritcu]

right, and "tentative fix to #N" and "does not fix #N" do too ... github is not so good with semantic differences :)

[catalin-hritcu]

Had a quick look at the 93 Z3 warnings this generates for the regression:

• 44 are invalid pop command, argument is greater than the current stack depth
• 32 are named expression already defined
• 15 are invalid declaration, function/constant ... (with the given signature) already declared
• 2 are Wrong number of arguments (2) passed to function (declare-fun Unification.nat_order () Term)

[nikswamy]

Yep. I'm aware of it. Thanks for logging

[nikswamy]

Down to 1 warning from an encoding glitch in FStar.DM4F.ST

[catalin-hritcu]

Just for the record, the remaining warning seems to be this one:

unknown(0,0-0,0) (Warning): FStar.DM4F.ST: Unexpected output from Z3: (error "line 36871 column 0: unknown constant @x4")

This looks like a similar problem to what I was getting with Simon when opening this bug. That's great progress.

[catalin-hritcu]

@nikswamy: Could it be that this last problem was inadvertently fixed recently? I can no longer reproduce it. FStar.DM4F.ST no longer raises this warning and nothing in our whole test suite does. Can we call this fixed? :)

[nikswamy]

Yes. I fixed some scoping bugs in dmff.fs the other day

[catalin-hritcu]

This kind of error is back in FStar.SquashProperties:

[hritcu@detained ulib]$ fstar.exe FStar.SquashProperties.fst
unknown(0,0-0,0): (Warning) FStar.SquashProperties: Unexpected output from Z3: (error "line 43541 column 43: unknown constant @x8")

[catalin-hritcu]

Closed in favor of #836, which has a simpler test case.