Method solve_expression

src/analysis/z3_solver.rs:95–101

Solve a Z3 ast without changing the internal state of the solver

(&self, expression: &Z3Expression)

    /// Solve a Z3 ast without changing the internal state of the solver
    pub fn solve_expression(&self, expression: &Z3Expression) -> SmtResult {
        self.set_backtrack_position();
        self.assert(expression);
        let result = self.solve();
        self.backtrack();
        result
    }

    /// Add a constraint into the solver
    pub fn assert(&self, expression: &Z3Expression) {