diff --git a/CreuSAT/src/logic/logic.rs b/CreuSAT/src/logic/logic.rs index 8cc03af9..087e65f4 100644 --- a/CreuSAT/src/logic/logic.rs +++ b/CreuSAT/src/logic/logic.rs @@ -1,4 +1,3 @@ -extern crate creusot_contracts; use creusot_contracts::std::*; use creusot_contracts::*; @@ -6,6 +5,16 @@ use crate::{assignments::*, clause::*, formula::*, lit::*, trail::*}; use crate::logic::{logic_assignments::*, logic_clause::*, logic_formula::*, logic_trail::*}; + +#[cfg(feature="contracts")] +mod inner { + struct Model(Mapping); + +} + +#[cfg(feature="contracts")] +pub use inner::*; + #[logic] fn pos() -> AssignedState { 1u8