Commit c50bfaa4 authored by Marek Chalupa's avatar Marek Chalupa
Browse files

sestate: re-implement is_feasible

We tried to ask whether constraints are sat given the assumption
that they are sat.
parent d9327e49
Loading
Loading
Loading
Loading
+12 −1
Original line number Diff line number Diff line
@@ -112,7 +112,18 @@ class SEState(ExecutionState):
        Solve the PC and return True if it is sat. Handy in the cases
        when the state is constructed manually.
        """
        return self.is_sat(*self.constraints())
        C = self.constraints()
        if not C:
            return True
        r = self._solver.try_is_sat(1000, *C)
        if r is not None:
            return r

        em = self.expr_manager()
        r = try_solve_incrementally([], C, em)
        if r is not None:
            return r
        return self._solver.is_sat(em.conjunction(*C))

    def concretize(self, *e):
        return self._solver.concretize(self.constraints(), *e)