Function haybale::solver_utils::bvs_can_be_equal

pub fn bvs_can_be_equal<V: BV>(btor: &Btor, a: &V, b: &V) -> Result<bool>

Returns true if under the current constraints, a and b can have the same value. Returns false if a and b cannot have the same value. (If the current constraints are themselves unsatisfiable, that will also result in false.)

A common use case for this function is to test whether some BV can be equal to a given concrete value. You can do this with something like bvs_can_be_equal(btor, bv, BV::from_u64(...)).

This function and bvs_must_be_equal() are both more efficient than get_a_solution() or get_possible_solutions()-type functions, as they do not require full model generation. You should prefer this function or bvs_must_be_equal() if they are sufficient for your needs.