diff --git a/.gitignore b/.gitignore index 908fcb0..e359ec8 100644 --- a/.gitignore +++ b/.gitignore @@ -20,3 +20,5 @@ run_nagini.py /tmp results results/* +/log_tries/ +/log_tries/* diff --git a/benchesResults/Nagini-Bench/tries_16_09.json b/benchesResults/Nagini-Bench/tries_16_09.json deleted file mode 100644 index ed720cb..0000000 --- a/benchesResults/Nagini-Bench/tries_16_09.json +++ /dev/null @@ -1,43 +0,0 @@ -{ - "005-intersperse.py": 4, - "009-rolling-max.py": 3, - "011-string_xor.py": 2, - "016-count_distinct_characters.py": 2, - "023-strlen.py": 0, - "024-largest-divisor.py": 2, - "027-flip_case.py": 3, - "029-filter_by_prefix.py": 3, - "035-max-element.py": 4, - "041-car_race_collision.py": 0, - "042-incr-list.py": 2, - "046-fib4.py": 3, - "050-encode_shift.py": 2, - "052-below-threshold.py": 2, - "053-add.py": 0, - "054-same-chars.py": 0, - "055-fib.py": 2, - "059-largest-prime-factor.py": 2, - "060-sum-to-n.py": 5, - "062-derivative.py": 2, - "063-fibfib.py": 4, - "066-digitSum.py": 4, - "082-prime-length.py": 2, - "083-starts_one_ends.py": 0, - "084-solve.py": 2, - "085-add.py": 2, - "092-any_int.py": 0, - "093-encode.py": 2, - "097-multiply.py": 0, - "098-count_upper.py": 3, - "100-make_a_pile.py": 3, - "110-exchange.py": 0, - "121-solution.py": 2, - "127-intersection.py": 0, - "134-check_if_last_char_is_a_letter.py": 0, - "138_is_equal_to_sum_even.py": 0, - "139-special_factorial.py": 3, - "146_specialFilter.py": 5, - "150-x_or_y.py": 4, - "157-right_angle_triangle.py": 0, - "159-eat.py": 0 -} \ No newline at end of file diff --git a/verified_cogen/tools/verifier.py b/verified_cogen/tools/verifier.py index 274a14b..b11aa5a 100644 --- a/verified_cogen/tools/verifier.py +++ b/verified_cogen/tools/verifier.py @@ -15,13 +15,20 @@ def __init__(self, shell: str, verifier_cmd: str, timeout: int = 60): self.timeout = timeout def verify(self, file_path: Path) -> Optional[tuple[bool, str, str]]: - proc = subprocess.Popen( - [self.shell, "-i", "-l", "-c", f'{self.verifier_cmd} "{file_path}"'], - stdout=subprocess.PIPE, - stderr=subprocess.PIPE, - ) try: - out, err = proc.communicate(timeout=self.timeout) - return proc.returncode == 0, out.decode(), err.decode() + res = subprocess.run( + '{} -i -l -c "{} "{}""; exit'.format( + self.shell, self.verifier_cmd, file_path + ), + capture_output=True, + shell=True, + timeout=self.timeout, + ) except subprocess.TimeoutExpired: - os.killpg(os.getpgid(proc.pid), signal.SIGTERM) + os.system("killall z3") + return None + return ( + res.returncode == 0, + res.stdout.decode("utf-8"), + res.stderr.decode("utf-8"), + )