(self, mgr=None)
return _And(stack)
Returns the last formula of the execution of the Script.

        This coincides with the conjunction of the assertions that are
        left on the assertion stack at the end of the SMTLibScript.
Returns the last formula of the execution of the Script.
Returns the last formula of the execution of the Script .
def get_last_formula(self, mgr=None):
        """Returns the last formula of the execution of the Script.

        This coincides with the conjunction of the assertions that are
        left on the assertion stack at the end of the SMTLibScript.
        """
        stack = []
        backtrack = []
        _And = mgr.And if mgr else get_env().formula_manager.And

        for cmd in self.commands:
            if cmd.name == smtcmd.ASSERT:
                stack.append(cmd.args[0])
            if cmd.name == smtcmd.RESET_ASSERTIONS:
                stack = []
                backtrack = []
            elif cmd.name == smtcmd.PUSH:
                for _ in range(cmd.args[0]):
                    backtrack.append(len(stack))
            elif cmd.name == smtcmd.POP:
                for _ in range(cmd.args[0]):
                    l = backtrack.pop()
                    stack = stack[:l]

        return _And(stack)
def get_last_formula ( self , mgr = None ) : stack = [ ] backtrack = [ ] _And = mgr . And if mgr else get_env ( ) . formula_manager . And for cmd in self . commands : if cmd . name == smtcmd . ASSERT : stack . append ( cmd . args [ 0 ] ) if cmd . name == smtcmd . RESET_ASSERTIONS : stack = [ ] backtrack = [ ] elif cmd . name == smtcmd . PUSH : for _ in range ( cmd . args [ 0 ] ) : backtrack . append ( len ( stack ) ) elif cmd . name == smtcmd . POP : for _ in range ( cmd . args [ 0 ] ) : l = backtrack . pop ( ) stack = stack [ : l ] return _And ( stack )