diff --git a/smtlib/src/solver.rs b/smtlib/src/solver.rs index b7f45b5..a483873 100644 --- a/smtlib/src/solver.rs +++ b/smtlib/src/solver.rs @@ -131,7 +131,7 @@ where } /// Adds soft-constraint `b` to the solver. - pub fn assert_soft(&mut self, b: Bool) -> Result<(), Error> where S: Sorted { + pub fn assert_soft(&mut self, b: Bool) -> Result<(), Error> { let term = b.into(); self.declare_all_consts(&term)?;