hasEq causes unknown constant in Z3 encoding

[s-zanella]

module M

#set-options "--log_queries"

let foo t = a:t{False}
let b:nat = 0

unknown(0,0-0,0): (Warning) M: Unexpected output from Z3: (error "line 48299 column 20: unknown constant @x0")

Such warnings usually hint to more profound issues.
This is also annoying because by default Emacs pops up a new window to display the Warnings buffer.

[catalin-hritcu]

Could this be the same as the last occurrence of #248?
#248 (comment)

[s-zanella]

Looks like the same problem. Should we close one of the issues?
The above example is much simpler than the warning from FStar.SquashProperties.l1, so it'll be good to keep it.

[catalin-hritcu]

Closed #248, let's just remember to also test on FStar.SquashProperties before closing this.

[catalin-hritcu]

@aseemr-msr The problem seems to be caused by hasEq. The bad part of the proof obligation looks like this:

;;;;;;;;;;;;;;;;haseq for Tm_refine_f1ecc6ab6882a651504f328937700647
(assert (!
         (iff (Valid (Prims.hasEq Tm_refine_f1ecc6ab6882a651504f328937700647))
              (Valid (Prims.hasEq @x0)))
         :named haseqTm_refine_f1ecc6ab6882a651504f328937700647))

[s-zanella]

Similar warning in FStar.List.Tot.Properties:

:pattern ((Valid (Prims.hasEq (Tm_refine_fb308c93c1a1992ab5d740874d192137 @x0))))))
:named haseqTm_refine_fb308c93c1a1992ab5d740874d192137))
(declare-fun Tm_abs_7c4549af84c08cffcaeaccd6eb5d4fd9 (Term Term) Term)
;;;;;;;;;;;;;;;;typing_Tm_abs_7c4549af84c08cffcaeaccd6eb5d4fd9
(assert (!
(forall ((@x0 Term) (@x1 Term))
 (! (HasType (Tm_abs_7c4549af84c08cffcaeaccd6eb5d4fd9 @x0
@x1)
(Tm_arrow_3fb06a3e5d4bcdefefe0aa3d3224bd9f Prims.unit
@x9
@x0
@x1))

[aseemr]

Fixed the hasEq related bug, it was not related to hasEq actually, there was a problem in the encoding of refinement types when the refinement is False, because of short circuit behavior.

Closing this, List.Tot.Properties seems unrelated, and is tracked in #844.