Closed puyral closed 1 year ago
Thanks @puyral!
with_type e t
is quite special and is emitted in F's encoding to SMT at specific points where the typechecker has proven internally that e
has type t
. F disables model-based quantifier instantiation (MBQI) in Z3 and relies, especially for cases like this, on pattern-based quantifier instantiation. Indeed, even in your minimized SMT2 file, if you add (as F* does) (set-option :smt.mbqi false) (set-option :auto-config false)
, Z3 says unknown.
That said, as you point out, when seen as an axiom on its own, it is clearly unsound. Rather than relying on quantifier triggers, we should see if there's a way to remove the with_type construction altogether. Especially if that would enable F* to be used with vampire, that would be really nice. Stay tuned, we'll look into what it takes to remove with_type.
This was more or less unused, I removed it and pushed the changes to the master branch. Closing this issue, please reopen if needed. Thanks!
Hello,
I've been trying recently, out of curiosity, to change
fstar
's backend fromz3
tovampire
. I made the discovery thatvampire
is able to deduceunsat
from anyfstar
file.The bug in general
Here are the steps to reproduce:
fstar
file that leads to the generation of ansmt
file when using#push-options "--log_queries"
smt
file moresmt
compliant, that is(declare-sort Term)
becomes(declare-sort Term 0)
(declare-datatypes () ((Fuel (ZFuel) (SFuel (prec Fuel)))))
becomes(declare-datatypes ((Fuel 0) (((ZFuel) (SFuel (prec Fuel)))))
implies
into=>
and anyiff
into=
echo
(this may be a limitation forvampire
)When this is done,
vampire
always returns:A suspicious axiom
Looking deeper, I could find one suspicious axiom:
If I understand correctly, with this axiom, it is possible to prove that anything has any type.
A minimal example
From the following
fstar
programI can extract the following axioms and declaration:
And then even
z3
provesunsat