From 3c7dba31d502e3e274e5959544083e5a20f6dbdc Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Wed, 27 Dec 2017 21:41:52 +0000 Subject: [PATCH] Termination condition for max_level --- smt/smt_checker_rsc_param.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/smt/smt_checker_rsc_param.py b/smt/smt_checker_rsc_param.py index c1dd3ca..d424dcc 100644 --- a/smt/smt_checker_rsc_param.py +++ b/smt/smt_checker_rsc_param.py @@ -775,6 +775,10 @@ class SmtCheckerRSCParam(object): print_info("UNSAT") 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) # assertions for all the paths @@ -787,10 +791,6 @@ class SmtCheckerRSCParam(object): 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: self.print_time(start_time) if print_mem: