artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Termination condition for max_level

Browse Source
This commit is contained in:
Artur Meski
2017-12-27 21:41:52 +00:00
parent 8d89047941
commit 3c7dba31d5
1 changed files with 4 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
smt/smt_checker_rsc_param.py
View File

@@ -775,6 +775,10 @@ class SmtCheckerRSCParam(object):
print_info("UNSAT") print_info("UNSAT")
self.solver.pop() self.solver.pop()
if not max_level is None and self.current_level > max_level:
print_info("As requested, stopping at level=" + str(max_level))
break
self.prepare_all_variables(num_of_paths) self.prepare_all_variables(num_of_paths)
# assertions for all the paths # assertions for all the paths
@@ -787,10 +791,6 @@ class SmtCheckerRSCParam(object):
self.current_level += 1 self.current_level += 1
if not max_level is None and self.current_level > max_level:
print_info("Stopping at level=" + str(max_level))
break
if print_time: if print_time:
self.print_time(start_time) self.print_time(start_time)
if print_mem: if print_mem: