pub fn sat_with_extra_constraints<I, B>(
    btor: &Btor,
    constraints: impl IntoIterator<Item = I>
) -> Result<bool>where
    I: Deref<Target = B>,
    B: BV,
Expand description

Returns true if the current constraints plus the additional constraints conds are together satisfiable, or false if not.

Returns Error::SolverError if the query failed (e.g., was interrupted or timed out).

Does not permanently add the constraints in conds to the solver.