curiosity lowering boolean variable in definition

[graydon]

Here is a reduced testcase that fails ivy_check:

#lang ivy1.7
object foobar = {
    relation foo(BAR:bool)
    definition foo(BAR:bool) = true
    invariant forall BAR. foo(BAR)
} 

ivy_check crashes with an assert False after emitting bad fmla: Var('BAR', BooleanSort()) inside formula_to_z3_int. It doesn't seem to like the BAR variable inside the definition of foo.

This version (with bar:bool in the definition) works:

#lang ivy1.7
object foobar = {
    relation foo(BAR:bool)
    definition foo(bar:bool) = true
    invariant forall BAR. foo(BAR)
} 

As does this version (with a 2-element non-bool type):

#lang ivy1.7
type booly = {truey, falsey}
object foobar = {
    relation foo(BAR:booly)
    definition foo(BAR:booly) = true
    invariant forall BAR. foo(BAR)
}