laws with unsatisfied where clauses shouldn't be loaded

[xldenis]

in the following program:

extern crate creusot_contracts;
use creusot_contracts::*;

trait A {
    #[logic]
    fn a(self) -> Option<()>;

    #[law]
    #[ensures(self.a() != None)]
    fn a_b(self) where Self: B;
}

trait B : A {}

impl A for () {
    #[logic]
    fn a(self) -> Option<()> { Some(()) }

    #[law]
    #[ensures(self.a() != None)]
    fn a_b(self) { }
}

fn x() {
    proof_assert! { ().a() == Some(()) }
}

the function x will load the law a_b even though B is not implemented. I haven't yet used this to prove false, but this is such a glaring issue that i'm sure someone slightly more motivated could find a way.

[xldenis]

Obviously, when we attempt to load a law we should check that its predicates are satisfied.