Method check_assert_condition

src/checker/assertion_checker.rs:141–182

(
        &self,
        cond: Rc<SymbolicValue>,
        expect: bool,
        abstract_value: &AbstractDomain<DomainType>,
    )

    }

    pub fn check_assert_condition(
        &self,
        cond: Rc<SymbolicValue>,
        expect: bool,
        abstract_value: &AbstractDomain<DomainType>,
    ) -> CheckerResult {
        let solver = &self.body_visitor.z3_solver;

        Self::add_numerical_constraints(&solver, abstract_value);

        let result;
        debug!("In converting assertion condition: {:?}", cond);
        let z3_cond_expr = if expect == false {
            solver.make_not_z3_expression(
                solver.convert_to_bool_sort(solver.get_symbolic_as_z3_expression(&cond)),
            )
        } else {
            solver.convert_to_bool_sort(solver.get_symbolic_as_z3_expression(&cond))
        };
        match solver.solve_expression(&z3_cond_expr) {
            SmtResult::Unsat => {
                // assert is always false
                result = CheckerResult::Unsafe;
            }
            SmtResult::Sat => {
                // assert is satisfiable, now check whether `not cond_val` is always false
                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
                    result = CheckerResult::Safe;
                } else {
                    result = CheckerResult::Warning;
                }
            }
            SmtResult::Unknown => {
                result = CheckerResult::Warning;
            }
        }
        solver.reset();

        result
    }

    // Add constraints from the numerical abstract domain
    fn add_numerical_constraints(solver: &Z3Solver, abstract_value: &AbstractDomain<DomainType>) {