setting a time out

[aalhuz]

Hi, I am running the solver for thousands of files. The issue is that for some files that solver takes forever to terminate. Is there a way to set a time out in the wrapper python script.

Thanks

[GroundPound]

I use the Linux timeout command and then check the status code to see if it was an actual timeout. If you are using a recent version of Python 3, then you can modify the subprocess calls in the wrapper script to use the optional timeout argument.

[z3str]

Thanks, @GroundPound! Exactly.

The following is a relevant python snippet we used in testing.

def run(args, cwd = None, shell = False, kill_tree = True, timeout = -1, env = None):
    '''
    Run a command with a timeout after which it will be forcibly
    killed.
    '''
    class Alarm(Exception):
        pass
    def alarm_handler(signum, frame):
        raise Alarm
    p = Popen(args, shell = shell, cwd = cwd, stdout = PIPE, stderr = PIPE, env = env)
    if timeout != -1:
        signal(SIGALRM, alarm_handler)
        alarm(timeout)
    try:
        stdout, stderr = p.communicate()
        if timeout != -1:
            alarm(0)
    except Alarm:
        pids = [p.pid]
        if kill_tree:
            pids.extend(get_process_children(p.pid))
        for pid in pids:
            # process might have died before getting to this line
            # so wrap to avoid OSError: no such process
            try: 
                kill(pid, SIGKILL)
            except OSError:
                pass
        return -9, '', ''
    return p.returncode, stdout, stderr

def run_z3str(fileName,timeout):

    testFile=test_dir+'/'+fileName

    startTime=time.time()

    exit_code,output,errors=run(solver_name+' '+testFile,shell=True,timeout=timeout)

    endTime=time.time()
    timeTaken=round(float(endTime-startTime), 3)