INNER CODE UNIT · Python

checkUNSAT

stp/stp · scripts/fuzz/fuzz_test.py:221

    def checkUNSAT(self, fname):
        # execute with the other solver
        toexec = "%s %s" % (options.checker, fname)
        print("Solving with other solver.. '%s'" % toexec)
        currTime = time.time()
        p = subprocess.Popen(toexec.rsplit(), stdout=subprocess.PIPE,
                             universal_newlines=True, preexec_fn=setlimits)
        consoleOutput2 = p.communicate()[0]

        # if other solver was out of time, then we can't say anything
        diffTime = time.time() - currTime
        if diffTime > maxTime-maxTimeDiff:
            print("Other solver: too much time to solve, aborted!")
            return None

        # extract output from the other solver
        print("Checking other solver output...")
        (otherSolverUNSAT, otherSolverValue) = self.parse_solution_from_output(consoleOutput2.split("\n"))

View source record →