"Boolean Programs" Model-Checked in Dice

# hack to allow us to use non-functional probabilistic ITE
Base.ifelse(::Dist{Bool}, ::Any, ::Nothing) = DistUInt32(77)
Base.ifelse(::Dist{Bool}, ::Nothing, ::Any) = DistUInt32(77)

choice() = flip(0.5)

function main()
    c1, c2 = choice(), choice()
    y = c1

    function getUnit()
        x = false
        if y
            if c2
                y = false  # deleting this causes a ProbException (as it should)
                x = true
            end
        else
            x = true
        end

        if x
            if y
                error("assert(F)")
            end
        end
        true
    end

    getUnit()
    false  # dummy return value
end

md = @dice main()
pr(md)