Method solve_condition

src/analysis/mir_visitor/block_visitor.rs:3498–3534

(&mut self, cond_val: &Rc<SymbolicValue>)

    }

    fn solve_condition(&mut self, cond_val: &Rc<SymbolicValue>) -> Option<bool> {
        let constraint_system = LinearConstraintSystem::from(&self.state().numerical_domain);

        let sat;
        let solver = &self.body_visitor.z3_solver;
        for cst in &constraint_system {
            debug!("Adding numerical constraint to SMT solver: {:?}", cst);
            solver.assert(&solver.get_as_z3_expression(cst));
        }

        let z3_cond_expr =
            solver.convert_to_bool_sort(solver.get_symbolic_as_z3_expression(cond_val));

        match solver.solve_expression(&z3_cond_expr) {
            SmtResult::Unsat => {
                // `cond_val` is always false
                sat = Some(false);
            }
            SmtResult::Sat => {
                // `cond_val` is satisfiable, now check whether `not cond_val` is always false
                // cst = cst.negate();
                let cst = solver.make_not_z3_expression(z3_cond_expr);
                if solver.solve_expression(&cst) == SmtResult::Unsat {
                    // `not cond_val` is always false, so `cond_val` is always true
                    sat = Some(true);
                } else {
                    sat = None
                }
            }
            SmtResult::Unknown => {
                sat = None;
            }
        }
        solver.reset();

        sat
    }
}