diff --git a/copy_files_from_s1904.py b/copy_files_from_s1904.py new file mode 100644 index 00000000..d990e9ac --- /dev/null +++ b/copy_files_from_s1904.py @@ -0,0 +1,58 @@ +import os +import subprocess +import re + +# Define the directory containing the folders +base_dir = "data/dbs" + +# Define the remote base paths and the local base paths +remote_dbg_base_path = "yizhou7@serenity-9900k-9a78.andrew.cmu.edu:/home/yizhou7/mariposa/dbg" +local_dbg_base_path = "/home/amarshah/mariposa_fixed/mariposa/dbg" + +remote_proj_base_path = "yizhou7@serenity-9900k-9a78.andrew.cmu.edu:/home/yizhou7/mariposa/data/projs" +local_proj_base_path = "/home/amarshah/mariposa_fixed/mariposa/data/projs" + +remote_filtered_base_path = "yizhou7@serenity-9900k-9a78.andrew.cmu.edu:/home/yizhou7/mariposa/data/projs" +local_filtered_base_path = "/home/amarshah/mariposa_fixed/mariposa/data/projs" + +# Ensure the local directories exist +os.makedirs(local_dbg_base_path, exist_ok=True) +os.makedirs(local_proj_base_path, exist_ok=True) + +# Loop through all folders in the base directory +for folder_name in os.listdir(base_dir): + # Match folders of the form "singleton_{number}" + if folder_name.startswith("singleton_") and not folder_name.endswith(".filtered"): + number = folder_name[len("singleton_"):] + # First SCP command: Copy dbg files + remote_dbg_path = f"{remote_dbg_base_path}/{number}" + local_dbg_path = f"{local_dbg_base_path}" + dbg_command = ["scp", "-r", remote_dbg_path, local_dbg_path] + print(f"Running: {' '.join(dbg_command)}") + try: + subprocess.run(dbg_command, check=True) + except subprocess.CalledProcessError as e: + print(f"Error while running command: {' '.join(dbg_command)}") + print(e) + + # Second SCP command: Copy proj files + remote_proj_path = f"{remote_proj_base_path}/singleton_{number}" + local_proj_path = f"{local_proj_base_path}" + proj_command = ["scp", "-r", remote_proj_path, local_proj_path] + print(f"Running: {' '.join(proj_command)}") + try: + subprocess.run(proj_command, check=True) + except subprocess.CalledProcessError as e: + print(f"Error while running command: {' '.join(proj_command)}") + print(e) + + # Third SCP command: Copy filtered proj files + remote_filtered_path = f"{remote_filtered_base_path}/singleton_{number}.filtered" + local_filtered_path = f"{local_filtered_base_path}" + filtered_command = ["scp", "-r", remote_filtered_path, local_filtered_path] + print(f"Running: {' '.join(filtered_command)}") + try: + subprocess.run(filtered_command, check=True) + except subprocess.CalledProcessError as e: + print(f"Error while running command: {' '.join(filtered_command)}") + print(e) diff --git a/src/demo.ipynb b/src/demo.ipynb index e287aea7..a8214476 100755 --- a/src/demo.ipynb +++ b/src/demo.ipynb @@ -2,1657 +2,58 @@ "cells": [ { "cell_type": "code", - "execution_count": 1, + "execution_count": 4, "metadata": {}, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ - " 0%| | 0/70 [00:00 not found in dbg/199ba4594c/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/a1b4b3fd4a/proofs/rename.13466259782321760747.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/a1b4b3fd4a/traces/rename.16754898796465586930 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at f9149ae61a4b36d6396f9b5cf95f9e8b.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_689 not found in dbg/a1b4b3fd4a/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_861 not found in dbg/a1b4b3fd4a/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_1100 not found in dbg/a1b4b3fd4a/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_704 not found in dbg/a1b4b3fd4a/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_901 not found in dbg/a1b4b3fd4a/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_1081 not found in dbg/a1b4b3fd4a/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_652 not found in dbg/a1b4b3fd4a/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_981 not found in dbg/a1b4b3fd4a/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 3%|▎ | 2/70 [00:09<05:13, 4.61s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/a1b4b3fd4a/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/a1b4b3fd4a/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/7a3bd28b48/proofs/reseed.14033866900517707504.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/7a3bd28b48/traces/reseed.14297332801369262032 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 4abccf2acf7fa4249a3490d371096a65.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_1512 not found in dbg/7a3bd28b48/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_1817 not found in dbg/7a3bd28b48/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_1736 not found in dbg/7a3bd28b48/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_1693 not found in dbg/7a3bd28b48/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_1872 not found in dbg/7a3bd28b48/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_1898 not found in dbg/7a3bd28b48/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_1884 not found in dbg/7a3bd28b48/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_1459 not found in dbg/7a3bd28b48/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 4%|▍ | 3/70 [00:14<05:18, 4.75s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/7a3bd28b48/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/7a3bd28b48/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/0a3bc89db1/proofs/shuffle.4147418025328775426.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/0a3bc89db1/traces/reseed.2681355025314892744 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at a689f3d1d50b3114aa92ee989fc46c82.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_2336 not found in dbg/0a3bc89db1/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_2611 not found in dbg/0a3bc89db1/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_2752 not found in dbg/0a3bc89db1/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_2767 not found in dbg/0a3bc89db1/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_2369 not found in dbg/0a3bc89db1/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_2104 not found in dbg/0a3bc89db1/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_2740 not found in dbg/0a3bc89db1/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_2138 not found in dbg/0a3bc89db1/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 6%|▌ | 4/70 [00:19<05:35, 5.08s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/0a3bc89db1/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/0a3bc89db1/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/55b4af82a4/proofs/reseed.3229159264617141076.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/55b4af82a4/traces/reseed.2446138819067655487 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 6eefa14ea615713852190ba16e3a1f6a.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_3087 not found in dbg/55b4af82a4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_3460 not found in dbg/55b4af82a4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_3486 not found in dbg/55b4af82a4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_3499 not found in dbg/55b4af82a4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_3544 not found in dbg/55b4af82a4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_3529 not found in dbg/55b4af82a4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_3305 not found in dbg/55b4af82a4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_3218 not found in dbg/55b4af82a4/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 7%|▋ | 5/70 [00:24<05:20, 4.94s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/55b4af82a4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/55b4af82a4/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/2faba7bd1f/proofs/rename.7442955955131910745.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/2faba7bd1f/traces/rename.8561135289699441601 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at c67cbc7ea27b69ac82f437bab2fc5f74.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_4289 not found in dbg/2faba7bd1f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_4140 not found in dbg/2faba7bd1f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_4106 not found in dbg/2faba7bd1f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_4245 not found in dbg/2faba7bd1f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_4258 not found in dbg/2faba7bd1f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_4089 not found in dbg/2faba7bd1f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_3975 not found in dbg/2faba7bd1f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_4327 not found in dbg/2faba7bd1f/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 9%|▊ | 6/70 [00:28<05:07, 4.80s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/2faba7bd1f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/2faba7bd1f/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/68ac429152/proofs/reseed.13773627200691514412.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/68ac429152/traces/shuffle.1899044262579460870 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 2c9a4ef192626bd63cbab074fb02527b.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_4930 not found in dbg/68ac429152/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_4941 not found in dbg/68ac429152/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_4985 not found in dbg/68ac429152/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_4997 not found in dbg/68ac429152/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_4686 not found in dbg/68ac429152/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_4803 not found in dbg/68ac429152/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 10%|█ | 7/70 [00:32<04:38, 4.42s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/68ac429152/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/68ac429152/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/634ab613c3/proofs/reseed.3662638186649401493.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/634ab613c3/traces/shuffle.2969354737312180380 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 96e0f7cfdeec7080ec300906eff64e72.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_5488 not found in dbg/634ab613c3/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_5657 not found in dbg/634ab613c3/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_5319 not found in dbg/634ab613c3/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_5395 not found in dbg/634ab613c3/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_5511 not found in dbg/634ab613c3/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_5246 not found in dbg/634ab613c3/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_5255 not found in dbg/634ab613c3/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_5269 not found in dbg/634ab613c3/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_5290 not found in dbg/634ab613c3/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 11%|█▏ | 8/70 [00:37<04:52, 4.72s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/634ab613c3/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/634ab613c3/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/106770d98e/proofs/shuffle.9855462634288510796.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/106770d98e/traces/reseed.3851331470606154282 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 48755c30690ff2b0141ce7195ccff6cd.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_6360 not found in dbg/106770d98e/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_6318 not found in dbg/106770d98e/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_5994 not found in dbg/106770d98e/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_6128 not found in dbg/106770d98e/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_6270 not found in dbg/106770d98e/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_5868 not found in dbg/106770d98e/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 13%|█▎ | 9/70 [00:43<05:08, 5.05s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/106770d98e/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/106770d98e/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/48dbc6d4fa/proofs/rename.9972412628472097492.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/48dbc6d4fa/traces/reseed.10404193983173560533 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 419f6ea493bc11b263c7000f0306b065.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_6721 not found in dbg/48dbc6d4fa/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_7287 not found in dbg/48dbc6d4fa/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_6931 not found in dbg/48dbc6d4fa/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_7110 not found in dbg/48dbc6d4fa/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_7142 not found in dbg/48dbc6d4fa/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_6655 not found in dbg/48dbc6d4fa/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_7304 not found in dbg/48dbc6d4fa/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 14%|█▍ | 10/70 [00:48<04:51, 4.85s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/48dbc6d4fa/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/48dbc6d4fa/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/621abdd996/proofs/reseed.8414757691389669604.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/621abdd996/traces/reseed.1522886428156592486 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at a54f17326f923e868d7de4370f157df9.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_7960 not found in dbg/621abdd996/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_7949 not found in dbg/621abdd996/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_7935 not found in dbg/621abdd996/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_7742 not found in dbg/621abdd996/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_8103 not found in dbg/621abdd996/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_8266 not found in dbg/621abdd996/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 16%|█▌ | 11/70 [00:54<05:12, 5.31s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/621abdd996/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/621abdd996/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/65d90190b4/proofs/rename.10906674507986506692.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/65d90190b4/traces/reseed.13107811493817202244 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at af984c1f59de349ab18714216a803c19.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_9061 not found in dbg/65d90190b4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_9192 not found in dbg/65d90190b4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_9203 not found in dbg/65d90190b4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_9243 not found in dbg/65d90190b4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_9098 not found in dbg/65d90190b4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_8550 not found in dbg/65d90190b4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_9225 not found in dbg/65d90190b4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_8912 not found in dbg/65d90190b4/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 17%|█▋ | 12/70 [01:01<05:31, 5.72s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/65d90190b4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/65d90190b4/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/cf8c015bcb/proofs/reseed.3116045616228988404.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/cf8c015bcb/traces/reseed.14515881125856259207 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 0ff49e8840ba4b14bda575b85f3eaf24.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_9634 not found in dbg/cf8c015bcb/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_9835 not found in dbg/cf8c015bcb/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_9805 not found in dbg/cf8c015bcb/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_9679 not found in dbg/cf8c015bcb/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_9697 not found in dbg/cf8c015bcb/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_9963 not found in dbg/cf8c015bcb/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_9949 not found in dbg/cf8c015bcb/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_9576 not found in dbg/cf8c015bcb/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 19%|█▊ | 13/70 [01:05<05:02, 5.30s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/cf8c015bcb/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/cf8c015bcb/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/eccd7ce2d9/proofs/reseed.5064846399809973974.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/eccd7ce2d9/traces/rename.7278557073235958777 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at c21447d1f0ddc2842e367ad74c137a23.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_10718 not found in dbg/eccd7ce2d9/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_10778 not found in dbg/eccd7ce2d9/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_10767 not found in dbg/eccd7ce2d9/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_10405 not found in dbg/eccd7ce2d9/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_10829 not found in dbg/eccd7ce2d9/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_10522 not found in dbg/eccd7ce2d9/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_10279 not found in dbg/eccd7ce2d9/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_10643 not found in dbg/eccd7ce2d9/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 20%|██ | 14/70 [01:09<04:33, 4.89s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/eccd7ce2d9/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/eccd7ce2d9/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/b475a457a9/proofs/reseed.1744378247872484033.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/b475a457a9/traces/reseed.17215664013271804878 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at d1749c79757077f2b2314f07bc0c17aa.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_11006 not found in dbg/b475a457a9/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_11013 not found in dbg/b475a457a9/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_10976 not found in dbg/b475a457a9/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 21%|██▏ | 15/70 [01:17<05:17, 5.78s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/b475a457a9/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/b475a457a9/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/a7f5536a00/proofs/reseed.10179614699221370520.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/a7f5536a00/traces/reseed.6943587227848217496 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 1d06f9ec32b7245d85fed03a85261e7f.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_237 not found in dbg/a7f5536a00/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_320 not found in dbg/a7f5536a00/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_375 not found in dbg/a7f5536a00/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_231 not found in dbg/a7f5536a00/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 23%|██▎ | 16/70 [01:22<04:59, 5.54s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/a7f5536a00/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/a7f5536a00/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/b834736f4d/proofs/reseed.3130966654838922115.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/b834736f4d/traces/rename.12362528586306987492 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 4ac350ff694bdca85d8c99863045c160.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_11585 not found in dbg/b834736f4d/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_11775 not found in dbg/b834736f4d/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_11413 not found in dbg/b834736f4d/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_11530 not found in dbg/b834736f4d/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_11986 not found in dbg/b834736f4d/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_11472 not found in dbg/b834736f4d/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_11492 not found in dbg/b834736f4d/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_11434 not found in dbg/b834736f4d/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_11452 not found in dbg/b834736f4d/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 24%|██▍ | 17/70 [01:26<04:34, 5.18s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/b834736f4d/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/b834736f4d/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/4d2d4fbc20/proofs/shuffle.16912401156957085999.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/4d2d4fbc20/traces/rename.12461037147283411353 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 82a72da80fb19909556f01c9dd5212d2.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_12479 not found in dbg/4d2d4fbc20/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_12574 not found in dbg/4d2d4fbc20/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_12180 not found in dbg/4d2d4fbc20/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_12328 not found in dbg/4d2d4fbc20/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_12615 not found in dbg/4d2d4fbc20/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_12718 not found in dbg/4d2d4fbc20/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_12276 not found in dbg/4d2d4fbc20/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_12643 not found in dbg/4d2d4fbc20/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 26%|██▌ | 18/70 [01:30<04:13, 4.87s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/4d2d4fbc20/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/4d2d4fbc20/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/81b159a977/proofs/shuffle.5160420872713078138.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/81b159a977/traces/shuffle.13806555427178412518 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 042022234555be42bbc008cfa15d82a4.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_13282 not found in dbg/81b159a977/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_13007 not found in dbg/81b159a977/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 27%|██▋ | 19/70 [01:38<04:58, 5.86s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/81b159a977/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/81b159a977/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/66c9bdf69f/proofs/shuffle.11828432509569748923.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/66c9bdf69f/traces/reseed.13957856434642412621 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 7aeb6275a404201c1598bb900c2f182a.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_13967 not found in dbg/66c9bdf69f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_13827 not found in dbg/66c9bdf69f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_14242 not found in dbg/66c9bdf69f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_14038 not found in dbg/66c9bdf69f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_14056 not found in dbg/66c9bdf69f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_14085 not found in dbg/66c9bdf69f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_14071 not found in dbg/66c9bdf69f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_13755 not found in dbg/66c9bdf69f/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 29%|██▊ | 20/70 [01:43<04:29, 5.38s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/66c9bdf69f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/66c9bdf69f/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/93004876e4/proofs/reseed.2280866902240984510.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/93004876e4/traces/reseed.1837398607084254552 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 9b0a3113686344cfc9083ad34e7af076.pickle \u001b[0m\n", - " 31%|███▏ | 22/70 [01:45<02:47, 3.49s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/93004876e4/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/93004876e4/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/2045867a58/proofs/shuffle.1507159208044294623.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/2045867a58/traces/shuffle.1580687978232137444 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at fd2ed6d21e5c6ec00d150ee880f03185.pickle \u001b[0m\n", - " 33%|███▎ | 23/70 [01:46<02:07, 2.71s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/2045867a58/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/2045867a58/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/09d24c83cd/proofs/reseed.16561741523881799952.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/09d24c83cd/traces/shuffle.5558647200263296762 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at b33e13d3c5310419bf354d56a1209703.pickle \u001b[0m\n", - " 34%|███▍ | 24/70 [01:46<01:40, 2.19s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/09d24c83cd/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/09d24c83cd/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/6937ca47cd/proofs/shuffle.8676475921380800677.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/6937ca47cd/traces/reseed.16593544487877940751 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 7599a1b61ed6e7b9c60df33a629e7539.pickle \u001b[0m\n", - " 36%|███▌ | 25/70 [01:49<01:46, 2.36s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/6937ca47cd/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/6937ca47cd/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/82449bd2e8/proofs/shuffle.1824484889151391589.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/82449bd2e8/traces/rename.8223263913722026815 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 2b0baa4fbdbd43ba062946081e30f2e7.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_15070 not found in dbg/82449bd2e8/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 39%|███▊ | 27/70 [01:51<01:16, 1.78s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/82449bd2e8/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/82449bd2e8/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/6540edb885/proofs/reseed.16122103410385013002.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/6540edb885/traces/rename.13836234746097889101 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at bb0d4d00b8697a0173df7190d806b945.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_15497 not found in dbg/6540edb885/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 40%|████ | 28/70 [01:59<02:16, 3.25s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/6540edb885/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/6540edb885/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/b119384805/proofs/shuffle.16404986598649049499.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/b119384805/traces/reseed.2646657787367492671 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 42575617fc2c3d37ca7747c9f14eea58.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_15999 not found in dbg/b119384805/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 41%|████▏ | 29/70 [02:02<02:10, 3.19s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/b119384805/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/b119384805/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/0918f4a55d/proofs/shuffle.930416732880363094.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/0918f4a55d/traces/reseed.18009040895761984794 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at d060e20ecd878f496c29e325aab77c14.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_16200 not found in dbg/0918f4a55d/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 43%|████▎ | 30/70 [02:05<02:06, 3.16s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/0918f4a55d/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/0918f4a55d/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/aad03b9358/proofs/reseed.3470960531457555157.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/aad03b9358/traces/reseed.14685607622128194302 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at bd829a77d9e8379fdb2f1c676c5dbcff.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_16409 not found in dbg/aad03b9358/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_16775 not found in dbg/aad03b9358/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_16740 not found in dbg/aad03b9358/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_16760 not found in dbg/aad03b9358/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_16770 not found in dbg/aad03b9358/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 44%|████▍ | 31/70 [02:09<02:04, 3.19s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/aad03b9358/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/aad03b9358/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/8d058577cd/proofs/rename.9999379753263398590.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/8d058577cd/traces/shuffle.16031162538414592248 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at e471625220affba6fc9c32b2df8243dd.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_16850 not found in dbg/8d058577cd/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid unknown_16859 not found in dbg/8d058577cd/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 46%|████▌ | 32/70 [02:10<01:45, 2.78s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/8d058577cd/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/8d058577cd/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/83bd54cd1a/proofs/reseed.5526298263868232628.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/83bd54cd1a/traces/reseed.2707133698505971685 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at ff7db140d64ecbcf7d9747ea8218afd8.pickle \u001b[0m\n", - " 47%|████▋ | 33/70 [02:14<01:49, 2.97s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/83bd54cd1a/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/83bd54cd1a/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/2556504d15/proofs/reseed.14418273676470417676.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/2556504d15/traces/shuffle.2985516088065258878 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at c3bcde4a2e181c6c17f405b0dee16269.pickle \u001b[0m\n", - " 49%|████▊ | 34/70 [02:17<01:48, 3.01s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/2556504d15/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/2556504d15/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/c726bffe99/proofs/shuffle.17977778541949180340.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/c726bffe99/traces/rename.2631641013891346680 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 6c025c3bd0c9e0669a5617ff8457b4fb.pickle \u001b[0m\n", - " 50%|█████ | 35/70 [02:21<01:53, 3.24s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/c726bffe99/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/c726bffe99/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/f08610121f/proofs/shuffle.7394039751016159464.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/f08610121f/traces/reseed.17699498497585027666 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at cf589309e88f623ef03e6a307b9d6436.pickle \u001b[0m\n", - " 51%|█████▏ | 36/70 [02:24<01:55, 3.40s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/f08610121f/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/f08610121f/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/fdfae1157a/proofs/shuffle.3218465744839795938.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/fdfae1157a/traces/shuffle.4882204877945181955 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 406a65921612482e53d49ae44334622f.pickle \u001b[0m\n", - " 53%|█████▎ | 37/70 [02:28<01:53, 3.44s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/fdfae1157a/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/fdfae1157a/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/8c0bbf67d0/proofs/rename.9021218465525474810.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/8c0bbf67d0/traces/reseed.2926928540658751903 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 6437b1ebdab0b25eef3f848c1cb05aeb.pickle \u001b[0m\n", - " 54%|█████▍ | 38/70 [02:29<01:24, 2.63s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/8c0bbf67d0/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/f6f3f962c0/proofs/shuffle.13526046991560484318.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/f6f3f962c0/traces/shuffle.5345052648385214803 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at c4c1f6d166ad5b106554b653f12ed9c4.pickle \u001b[0m\n", - " 56%|█████▌ | 39/70 [02:29<00:59, 1.91s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/f6f3f962c0/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/9eaad8947e/proofs/reseed.345321281840103149.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/9eaad8947e/traces/rename.6382520140487459991 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at d77284012b937737531251067601c243.pickle \u001b[0m\n", - " 57%|█████▋ | 40/70 [02:31<00:59, 1.99s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/9eaad8947e/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/fef99080cd/proofs/shuffle.6237900668407489070.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/fef99080cd/traces/shuffle.3355901794255631888 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at ffd07c924df572029210d1f6a0892c49.pickle \u001b[0m\n", - " 60%|██████ | 42/70 [02:32<00:34, 1.24s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/fef99080cd/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/08719204aa/proofs/shuffle.12559045082206736741.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/08719204aa/traces/reseed.325235324506828228 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 46567d78739508efef162199f7702738.pickle \u001b[0m\n", - " 61%|██████▏ | 43/70 [02:41<01:25, 3.17s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/08719204aa/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/fa2fdaf6e0/proofs/reseed.9457796464287592495.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/fa2fdaf6e0/traces/reseed.978582254624960590 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 80f24d861e72aa17b634916edccd3549.pickle \u001b[0m\n", - " 63%|██████▎ | 44/70 [02:45<01:25, 3.30s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/fa2fdaf6e0/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/d057fff3f5/proofs/rename.17608056682826294385.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/d057fff3f5/traces/shuffle.227536422975727424 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at d9a6fd7885eb3eb6c413c53316a91f44.pickle \u001b[0m\n", - " 64%|██████▍ | 45/70 [02:45<01:01, 2.46s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/d057fff3f5/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/d6181053ff/proofs/shuffle.1879102912735967004.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/d6181053ff/traces/shuffle.15181022330680520267 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at bb177960ff0bf14e16b55d9b3b47a355.pickle \u001b[0m\n", - " 66%|██████▌ | 46/70 [02:45<00:44, 1.83s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/d6181053ff/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/c4ec60f8f9/proofs/rename.5376817467618622123.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/c4ec60f8f9/traces/shuffle.8091374896670368150 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at ada6a7de7f0acccd849332d4e658b8cc.pickle \u001b[0m\n" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid unknown_19840 not found in dbg/c4ec60f8f9/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - " 67%|██████▋ | 47/70 [02:46<00:35, 1.53s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/c4ec60f8f9/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/c4ec60f8f9/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/815f69b161/proofs/rename.2393776269027745053.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/815f69b161/traces/shuffle.17997689439100610842 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 61cdc8c8faf5feccb5532403895d207c.pickle \u001b[0m\n", - " 70%|███████ | 49/70 [02:46<00:19, 1.06it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/815f69b161/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/92c260e39d/proofs/reseed.18042481600280132582.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/92c260e39d/traces/shuffle.15241268561291675236 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 796d93655f0e5c4aa06882ea28046c48.pickle \u001b[0m\n", - " 71%|███████▏ | 50/70 [02:47<00:16, 1.21it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/92c260e39d/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/7d8c4302ab/proofs/reseed.9908923975124208297.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/7d8c4302ab/traces/shuffle.15513482486857776214 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at cce3dd987c131a5c430a27e224e9fdf1.pickle \u001b[0m\n", - " 73%|███████▎ | 51/70 [02:47<00:14, 1.35it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/7d8c4302ab/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/3c5c22d4a1/proofs/shuffle.6686661779536535792.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/3c5c22d4a1/traces/shuffle.6184657921392492698 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at b714f48ce4ec76bcdab0049f62aae014.pickle \u001b[0m\n", - " 74%|███████▍ | 52/70 [02:48<00:12, 1.49it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/3c5c22d4a1/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/025a074d17/proofs/rename.8846467334752358090.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/025a074d17/traces/shuffle.7366767861977757192 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at b6ae9d191b9dcf1a03f08d5c02972d6b.pickle \u001b[0m\n", - " 76%|███████▌ | 53/70 [02:48<00:10, 1.66it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/025a074d17/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/492704d0da/proofs/reseed.12570179510938305325.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/492704d0da/traces/shuffle.1768421775674796906 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 3e95b0804ef115c3d20a43d4b984a6d7.pickle \u001b[0m\n", - " 77%|███████▋ | 54/70 [02:48<00:08, 1.88it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/492704d0da/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/be920877ca/proofs/shuffle.9555299481395785809.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/be920877ca/traces/shuffle.14575692651422062579 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 7f3387739f00544be2dda14c996725b3.pickle \u001b[0m\n", - " 79%|███████▊ | 55/70 [02:49<00:07, 2.03it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/be920877ca/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/e1d2573021/proofs/shuffle.17707152865482721884.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/e1d2573021/traces/shuffle.6352221195065630423 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 05028b8c0ccbd709417e1188d158a4ff.pickle \u001b[0m\n", - " 80%|████████ | 56/70 [02:49<00:06, 2.12it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/e1d2573021/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/126f0f80f3/proofs/rename.3415372238567156677.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/126f0f80f3/traces/shuffle.7693207495078702026 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 4bb589b12f6a5be4023d5450d536664b.pickle \u001b[0m\n", - " 81%|████████▏ | 57/70 [02:50<00:05, 2.24it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/126f0f80f3/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/a896b920ca/proofs/rename.13547342595759592148.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/a896b920ca/traces/shuffle.3935504091054792581 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at b031de557bb34b4d198667b141063b1a.pickle \u001b[0m\n", - " 83%|████████▎ | 58/70 [02:50<00:06, 1.83it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/a896b920ca/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/b689a8d455/proofs/reseed.7960457643126824502.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/b689a8d455/traces/shuffle.9658684377955998061 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 95b0b9726492cef911ef8e41d6a43142.pickle \u001b[0m\n", - " 84%|████████▍ | 59/70 [02:58<00:27, 2.51s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/b689a8d455/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/b689a8d455/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/fa9020870d/proofs/rename.10925249071271673183.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/fa9020870d/traces/shuffle.17192080644200663547 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at cd3656d7d4fdc20fb6a96c66631f6118.pickle \u001b[0m\n", - " 86%|████████▌ | 60/70 [02:58<00:19, 1.91s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/fa9020870d/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/fa9020870d/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/090a2a7d67/proofs/reseed.7014106981689618503.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/090a2a7d67/traces/shuffle.10445631812693282071 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 41884a1c910ece84f3f54ae2e3ed76a2.pickle \u001b[0m\n", - " 87%|████████▋ | 61/70 [02:59<00:13, 1.52s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/090a2a7d67/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/090a2a7d67/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/89068d3f38/proofs/rename.10834735852581795764.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/89068d3f38/traces/shuffle.14572447043468962421 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 0380df320ecfcfd29f8f226633bef441.pickle \u001b[0m\n", - " 89%|████████▊ | 62/70 [02:59<00:09, 1.24s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/89068d3f38/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/89068d3f38/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/32eaf80bcc/proofs/reseed.4328406295992163345.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/32eaf80bcc/traces/shuffle.6910780131629932731 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 6c0e31fb6ae09e69fb226f7d33702f19.pickle \u001b[0m\n", - " 90%|█████████ | 63/70 [03:00<00:07, 1.03s/it]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/32eaf80bcc/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/32eaf80bcc/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/af029e0bc2/proofs/reseed.14508368194316142897.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/af029e0bc2/traces/shuffle.18377065096165493170 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 59146d8ee8c364cadc6534eb19ef6d2c.pickle \u001b[0m\n", - " 91%|█████████▏| 64/70 [03:00<00:05, 1.14it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/af029e0bc2/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/af029e0bc2/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/2078a24298/proofs/shuffle.5340712248063809690.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/2078a24298/traces/shuffle.8829542882092737644 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 49a287e28735f9b29bd82386e439cb06.pickle \u001b[0m\n", - " 93%|█████████▎| 65/70 [03:01<00:03, 1.34it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/2078a24298/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/2078a24298/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/ed912ce861/proofs/rename.4681486518489633438.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/ed912ce861/traces/shuffle.6336912347899983229 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 426d45039acc0fc89bf3e138ede2e9a0.pickle \u001b[0m\n", - " 94%|█████████▍| 66/70 [03:01<00:02, 1.51it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/ed912ce861/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/ed912ce861/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/c02ff41a27/proofs/reseed.4788160957913371286.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/c02ff41a27/traces/shuffle.4351452066286619603 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 8c33787feb4a79c3a41d5862ba953477.pickle \u001b[0m\n", - " 96%|█████████▌| 67/70 [03:02<00:01, 1.69it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/c02ff41a27/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/c02ff41a27/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/5a940edd1b/proofs/rename.9440889024953437337.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/5a940edd1b/traces/shuffle.2189555834201964502 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at edb237501a4f2607b38b8e9bddba4d27.pickle \u001b[0m\n", - " 97%|█████████▋| 68/70 [03:02<00:01, 1.72it/s]" - ] - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "\u001b[93m[WARN] [differ] qid constructor_accessor_axiom not found in dbg/5a940edd1b/orig.smt2 \u001b[0m\n", - "\u001b[93m[WARN] [differ] qid not found in dbg/5a940edd1b/orig.smt2 \u001b[0m\n" + " 0%| | 0/70 [00:00 not found in dbg/568e167040/orig.smt2 \u001b[0m\n" + "\u001b[92m[INFO] [init] query path: data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit__proof__helper_invariants__proof.9.smt2 \u001b[0m\n", + "\u001b[92m[INFO] [init] dbg root: dbg/199ba4594c \u001b[0m\n" ] }, { "name": "stderr", "output_type": "stream", "text": [ - "\u001b[94m[DEBUG] [edit] proof path: dbg/e16c5e8c0b/proofs/reseed.6878216073608319661.proof \u001b[0m\n", - "\u001b[94m[DEBUG] [edit] trace path: dbg/e16c5e8c0b/traces/shuffle.15919015838397219284 \u001b[0m\n", - "\u001b[94m[DEBUG] using cache at 4e0db7b8d8e3c44665f59e8ba103c029.pickle \u001b[0m\n", - "100%|██████████| 70/70 [03:04<00:00, 2.63s/it]" + "\u001b[94m[DEBUG] [term graph] 64997 nodes, 234175 edges, root @[h!392b5117] \u001b[0m\n", + "\u001b[94m[DEBUG] 41 nodes are unreachable! \u001b[0m\n", + " 0%| | 0/70 [00:13 not found in dbg/e16c5e8c0b/orig.smt2 \u001b[0m\n" - ] - }, - { - "name": "stderr", - "output_type": "stream", - "text": [ - "\n" + "ename": "KeyboardInterrupt", + "evalue": "", + "output_type": "error", + "traceback": [ + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mKeyboardInterrupt\u001b[0m Traceback (most recent call last)", + "Cell \u001b[0;32mIn[4], line 55\u001b[0m\n\u001b[1;32m 53\u001b[0m dbg \u001b[38;5;241m=\u001b[39m Debugger3(query)\n\u001b[1;32m 54\u001b[0m current_dbgs[query] \u001b[38;5;241m=\u001b[39m dbg\n\u001b[0;32m---> 55\u001b[0m \u001b[38;5;28;01massert\u001b[39;00m \u001b[43mdbg\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43meditor\u001b[49m \u001b[38;5;129;01mis\u001b[39;00m \u001b[38;5;129;01mnot\u001b[39;00m \u001b[38;5;28;01mNone\u001b[39;00m\n", + "File \u001b[0;32m~/mariposa_fixed/mariposa/src/debugger3.py:172\u001b[0m, in \u001b[0;36mDebugger3.editor\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 170\u001b[0m log_debug(\u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124m[edit] proof path: \u001b[39m\u001b[38;5;132;01m{\u001b[39;00m\u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mchosen_proof_path\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m\"\u001b[39m)\n\u001b[1;32m 171\u001b[0m log_debug(\u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124m[edit] trace path: \u001b[39m\u001b[38;5;132;01m{\u001b[39;00m\u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mchosen_trace_path\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m\"\u001b[39m)\n\u001b[0;32m--> 172\u001b[0m proof \u001b[38;5;241m=\u001b[39m \u001b[43mProofAnalyzer\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mfrom_proof_file\u001b[49m\u001b[43m(\u001b[49m\n\u001b[1;32m 173\u001b[0m \u001b[43m \u001b[49m\u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mchosen_proof_path\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mclear\u001b[49m\u001b[38;5;241;43m=\u001b[39;49m\u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43m__clear_proof_cache\u001b[49m\n\u001b[1;32m 174\u001b[0m \u001b[43m\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 175\u001b[0m trace \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39m_builder\u001b[38;5;241m.\u001b[39mget_trace_mutant_info(\u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mchosen_trace_path)\n\u001b[1;32m 176\u001b[0m \u001b[38;5;28;01massert\u001b[39;00m trace\u001b[38;5;241m.\u001b[39mhas_trace()\n", + "File \u001b[0;32m~/mariposa_fixed/mariposa/src/debugger/proof_analyzer.py:312\u001b[0m, in \u001b[0;36mProofAnalyzer.from_proof_file\u001b[0;34m(proof_path, clear)\u001b[0m\n\u001b[1;32m 310\u001b[0m m\u001b[38;5;241m.\u001b[39mupdate(\u001b[38;5;28mstr\u001b[39m(proof_path)\u001b[38;5;241m.\u001b[39mencode())\n\u001b[1;32m 311\u001b[0m pickle_name \u001b[38;5;241m=\u001b[39m m\u001b[38;5;241m.\u001b[39mhexdigest() \u001b[38;5;241m+\u001b[39m \u001b[38;5;124m\"\u001b[39m\u001b[38;5;124m.pickle\u001b[39m\u001b[38;5;124m\"\u001b[39m\n\u001b[0;32m--> 312\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m \u001b[43mload_cache_or\u001b[49m\u001b[43m(\u001b[49m\u001b[43mpickle_name\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;28;43;01mlambda\u001b[39;49;00m\u001b[43m:\u001b[49m\u001b[43m \u001b[49m\u001b[43mProofAnalyzer\u001b[49m\u001b[43m(\u001b[49m\u001b[43mproof_path\u001b[49m\u001b[43m)\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mclear\u001b[49m\u001b[43m)\u001b[49m\n", + "File \u001b[0;32m~/mariposa_fixed/mariposa/src/utils/cache_utils.py:28\u001b[0m, in \u001b[0;36mload_cache_or\u001b[0;34m(name, func, clear)\u001b[0m\n\u001b[1;32m 26\u001b[0m obj \u001b[38;5;241m=\u001b[39m load_cache(name)\n\u001b[1;32m 27\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m obj \u001b[38;5;129;01mis\u001b[39;00m \u001b[38;5;28;01mNone\u001b[39;00m \u001b[38;5;129;01mor\u001b[39;00m clear:\n\u001b[0;32m---> 28\u001b[0m obj \u001b[38;5;241m=\u001b[39m \u001b[43mfunc\u001b[49m\u001b[43m(\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 29\u001b[0m save_cache(name, obj)\n\u001b[1;32m 30\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m obj\n", + "File \u001b[0;32m~/mariposa_fixed/mariposa/src/debugger/proof_analyzer.py:312\u001b[0m, in \u001b[0;36mProofAnalyzer.from_proof_file..\u001b[0;34m()\u001b[0m\n\u001b[1;32m 310\u001b[0m m\u001b[38;5;241m.\u001b[39mupdate(\u001b[38;5;28mstr\u001b[39m(proof_path)\u001b[38;5;241m.\u001b[39mencode())\n\u001b[1;32m 311\u001b[0m pickle_name \u001b[38;5;241m=\u001b[39m m\u001b[38;5;241m.\u001b[39mhexdigest() \u001b[38;5;241m+\u001b[39m \u001b[38;5;124m\"\u001b[39m\u001b[38;5;124m.pickle\u001b[39m\u001b[38;5;124m\"\u001b[39m\n\u001b[0;32m--> 312\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m load_cache_or(pickle_name, \u001b[38;5;28;01mlambda\u001b[39;00m: \u001b[43mProofAnalyzer\u001b[49m\u001b[43m(\u001b[49m\u001b[43mproof_path\u001b[49m\u001b[43m)\u001b[49m, clear)\n", + "File \u001b[0;32m~/mariposa_fixed/mariposa/src/debugger/proof_analyzer.py:78\u001b[0m, in \u001b[0;36mProofAnalyzer.__init__\u001b[0;34m(self, file_path)\u001b[0m\n\u001b[1;32m 75\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39m__insts_under_qname: Dict[\u001b[38;5;28mstr\u001b[39m, QuantInstInfo] \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mdict\u001b[39m()\n\u001b[1;32m 77\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mproof_graph \u001b[38;5;241m=\u001b[39m nx\u001b[38;5;241m.\u001b[39mDiGraph()\n\u001b[0;32m---> 78\u001b[0m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43m__analyze_proof_nodes\u001b[49m\u001b[43m(\u001b[49m\u001b[43m)\u001b[49m\n", + "File \u001b[0;32m~/mariposa_fixed/mariposa/src/debugger/proof_analyzer.py:88\u001b[0m, in \u001b[0;36mProofAnalyzer.__analyze_proof_nodes\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 86\u001b[0m \u001b[38;5;28;01mcontinue\u001b[39;00m\n\u001b[1;32m 87\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mproof_graph\u001b[38;5;241m.\u001b[39madd_node(ref)\n\u001b[0;32m---> 88\u001b[0m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43m__analyze_proof_node\u001b[49m\u001b[43m(\u001b[49m\u001b[43mref\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mnode\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 90\u001b[0m \u001b[38;5;66;03m# root will likely be unit-resolution...\u001b[39;00m\n\u001b[1;32m 91\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mproof_graph\u001b[38;5;241m.\u001b[39madd_node(\u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mroot_ref)\n", + "File \u001b[0;32m~/mariposa_fixed/mariposa/src/debugger/proof_analyzer.py:115\u001b[0m, in \u001b[0;36mProofAnalyzer.__analyze_proof_node\u001b[0;34m(self, ref, node)\u001b[0m\n\u001b[1;32m 111\u001b[0m \u001b[38;5;28;01massert\u001b[39;00m name \u001b[38;5;129;01min\u001b[39;00m PROOF_GRAPH_RULES\n\u001b[1;32m 113\u001b[0m conclusion \u001b[38;5;241m=\u001b[39m node\u001b[38;5;241m.\u001b[39mchildren[\u001b[38;5;241m-\u001b[39m\u001b[38;5;241m1\u001b[39m]\n\u001b[0;32m--> 115\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;129;01mnot\u001b[39;00m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mis_proof_free\u001b[49m\u001b[43m(\u001b[49m\u001b[43mconclusion\u001b[49m\u001b[43m)\u001b[49m:\n\u001b[1;32m 116\u001b[0m log_warn(\u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mproof node conclusion is not grounded: \u001b[39m\u001b[38;5;132;01m{\u001b[39;00mref\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m\"\u001b[39m)\n\u001b[1;32m 117\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m\n", + "File \u001b[0;32m~/mariposa_fixed/mariposa/src/debugger/symbol_table.py:274\u001b[0m, in \u001b[0;36mTermTable.is_proof_free\u001b[0;34m(self, ron)\u001b[0m\n\u001b[1;32m 272\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28misinstance\u001b[39m(node, ProofNode):\n\u001b[1;32m 273\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m \u001b[38;5;28;01mFalse\u001b[39;00m\n\u001b[0;32m--> 274\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28;43misinstance\u001b[39;49m\u001b[43m(\u001b[49m\u001b[43mnode\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mAppNode\u001b[49m\u001b[43m)\u001b[49m:\n\u001b[1;32m 275\u001b[0m refs\u001b[38;5;241m.\u001b[39mextend(node\u001b[38;5;241m.\u001b[39mchildren)\n\u001b[1;32m 276\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m \u001b[38;5;28;01mTrue\u001b[39;00m\n", + "\u001b[0;31mKeyboardInterrupt\u001b[0m: " ] } ], @@ -1663,10 +64,7 @@ "import pandas as pd\n", "from z3 import set_param\n", "\n", - "os.chdir(\"/home/yizhou7/mariposa\")\n", - "\n", "from analysis.singleton_analyzer import SingletonAnalyzer\n", - "from base.factory import FACT\n", "from base.exper import Experiment\n", "from base.exper_analyzer import ExperAnalyzer\n", "from debugger3 import Debugger3\n", @@ -1674,6 +72,9 @@ "from benchmark_consts import *\n", "from debugger.informed_editor import InformedEditor\n", "\n", + "os.chdir(\"/home/amarshah/mariposa_fixed/mariposa/\")\n", + "from base.factory import FACT\n", + "\n", "SOLVER = FACT.get_solver(\"z3_4_13_0\")\n", "VERI_CFG = FACT.get_config(\"verify\")\n", "FILTER_CFG = FACT.get_config(\"verus_quick\")\n", @@ -1716,7 +117,7 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": null, "metadata": {}, "outputs": [], "source": [ @@ -1778,86 +179,9 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "+----+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+---------------+----------------+--------------------+--------------------+--------------+-------------+----------------+----------------+\n", - "| | query | root_quants | tested_edits | edits_stabilized | quants_test_rate | error_rate | pass_rate | timeout_rate | unknown_rate |\n", - "|----+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+---------------+----------------+--------------------+--------------------+--------------+-------------+----------------+----------------|\n", - "| 0 | data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit__proof__helper_invariants__proof.9.smt2 | 718 | 624 | 1 | 76.7409 | 1.92308 | 93.2692 | 4.80769 | 0 |\n", - "| 1 | data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit__proof__helper_invariants__validation.3.smt2 | 816 | 952 | 8 | 86.8873 | 3.46639 | 93.0672 | 3.46639 | 0 |\n", - "| 2 | data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit__proof__liveness__daemon_set_match__lemma_from_after_get_daemon_set_step_to_after_update_daemon_set_step.smt2 | 1191 | 1487 | 9 | 98.7406 | 1.34499 | 92.5353 | 6.1197 | 0 |\n", - "| 3 | data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit__proof__liveness__resource_match__lemma_from_after_get_resource_step_to_after_update_resource_step.smt2 | 1112 | 1465 | 47 | 98.741 | 1.43345 | 96.8601 | 1.70648 | 0 |\n", - "| 4 | data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__resource_match.5.smt2 | 899 | 717 | 29 | 68.9655 | 1.11576 | 92.7476 | 6.13668 | 0 |\n", - "| 5 | data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__resource_match.6.smt2 | 955 | 959 | 8 | 83.7696 | 1.45985 | 88.4254 | 10.1147 | 0 |\n", - "| 6 | data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__resource_match__lemma_from_after_get_resource_step_to_after_create_resource_step.smt2 | 901 | 711 | 3 | 67.9245 | 1.12518 | 98.1716 | 0.703235 | 0 |\n", - "| 7 | data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__proof__lemma_eventually_always_every_resource_create_request_implies_at_after_create_resource_step.smt2 | 1348 | 1590 | 23 | 96.4392 | 1.44654 | 93.522 | 5.03145 | 0 |\n", - "| 8 | data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__proof__lemma_eventually_always_object_in_response_at_after_create_resource_step_is_same_as_etcd.smt2 | 1339 | 1640 | 60 | 98.4317 | 2.2561 | 85.8537 | 11.8293 | 0.0609756 |\n", - "| 9 | data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__validation__lemma_always_stateful_set_in_create_request_msg_satisfies_unchangeable.smt2 | 1431 | 1930 | 2 | 98.6024 | 1.39896 | 67.2021 | 31.399 | 0 |\n", - "| 10 | data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__resource_match.1.smt2 | 1221 | 1788 | 1 | 98.4439 | 1.06264 | 88.7584 | 10.179 | 0 |\n", - "| 11 | data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__resource_match__lemma_from_after_get_resource_step_to_after_update_resource_step.smt2 | 1225 | 1632 | 0 | 98.8571 | 1.28676 | 77.6348 | 21.0784 | 0 |\n", - "| 12 | data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__stateful_set_match__lemma_from_after_get_stateful_set_step_to_after_update_stateful_set_step.smt2 | 1454 | 1733 | 4 | 98.1431 | 1.09636 | 92.614 | 6.28967 | 0 |\n", - "| 13 | data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__stateful_set_match__lemma_stateful_set_state_matches_at_after_update_stateful_set_step.smt2 | 1467 | 1899 | 1 | 99.182 | 1.05319 | 93.6282 | 5.31859 | 0 |\n", - "| 14 | data/projs/anvil/base.z3/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof.2.smt2 | 688 | 564 | 11 | 76.0174 | 0.35461 | 98.9362 | 0.70922 | 0 |\n", - "| 15 | data/projs/anvil/base.z3/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof__lemma_always_no_update_status_request_msg_in_flight_of_except_stateful_set.smt2 | 1297 | 1549 | 218 | 96.2992 | 0.839251 | 98.7734 | 0.387347 | 0 |\n", - "| 16 | data/projs/anvil/base.z3/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof__lemma_eventually_always_no_delete_resource_request_msg_in_flight.smt2 | 1364 | 1543 | 17 | 92.8886 | 1.29618 | 97.9909 | 0.712897 | 0 |\n", - "| 17 | data/projs/anvil/base.z3/zookeeper-smt-zookeeper_controller__proof__helper_invariants__validation.3.smt2 | 840 | 978 | 24 | 87.5 | 3.37423 | 94.9898 | 1.63599 | 0 |\n", - "| 18 | data/projs/anvil/base.z3/zookeeper-smt-zookeeper_controller__proof__helper_invariants__zookeeper_api__lemma_zk_request_implies_step_helper.smt2 | 1226 | 1664 | 130 | 100 | 0.360577 | 97.6562 | 1.92308 | 0.0600962 |\n", - "| 19 | data/projs/anvil/base.z3/zookeeper-smt-zookeeper_controller__proof__liveness__stateful_set_match.2.smt2 | 1274 | 1225 | 3 | 75.8242 | 0.979592 | 94.2857 | 4.73469 | 0 |\n", - "| 20 | data/projs/flowcert/base.z3/permission.14.smt2 | 156 | 221 | 0 | 98.0769 | 2.71493 | 83.2579 | 13.1222 | 0.904977 |\n", - "| 21 | data/projs/splinterdb/base.z3/allocation_layer__LikesBetree_v.18.smt2 | 155 | 189 | 93 | 91.6129 | 4.2328 | 95.7672 | 0 | 0 |\n", - "| 22 | data/projs/splinterdb/base.z3/allocation_layer__LikesBetree_v__LikesBetree.3.smt2 | 297 | 419 | 121 | 96.9697 | 2.86396 | 94.2721 | 0 | 2.86396 |\n", - "| 23 | data/projs/verismo.dedup/base.z3/allocator__linkedlist.10.smt2 | 307 | 460 | 8 | 99.3485 | 2.6087 | 85.8696 | 11.5217 | 0 |\n", - "| 24 | data/projs/verismo.dedup/base.z3/boot__init__e820_init.2.smt2 | 304 | 112 | 5 | 33.2237 | 0.892857 | 80.3571 | 18.75 | 0 |\n", - "| 25 | data/projs/verismo.dedup/base.z3/boot__init__e820_init.4.smt2 | 517 | 699 | 46 | 98.2592 | 8.58369 | 90.4149 | 1.00143 | 0 |\n", - "| 26 | data/projs/verismo.dedup/base.z3/boot__init__e820_init_alloc.1.smt2 | 522 | 711 | 7 | 98.0843 | 3.09423 | 92.4051 | 4.5007 | 0 |\n", - "| 27 | data/projs/verismo.dedup/base.z3/bsp__ap.3.smt2 | 437 | 504 | 23 | 100 | 2.18254 | 95.2381 | 2.57937 | 0 |\n", - "| 28 | data/projs/verismo.dedup/base.z3/pgtable_e__pte.18.smt2 | 679 | 984 | 2 | 99.7054 | 3.65854 | 89.4309 | 6.91057 | 0 |\n", - "| 29 | data/projs/verismo.dedup/base.z3/pgtable_e__pte.20.smt2 | 423 | 454 | 1 | 98.818 | 0.440529 | 95.3744 | 0 | 4.18502 |\n", - "| 30 | data/projs/verismo.dedup/base.z3/security__monitor.21.smt2 | 715 | 872 | 3 | 100 | 4.47248 | 94.7248 | 0.802752 | 0 |\n", - "| 31 | data/projs/verismo.dedup/base.z3/snp__cpuid.17.smt2 | 551 | 678 | 32 | 100 | 3.24484 | 96.0177 | 0.737463 | 0 |\n", - "| 32 | data/projs/verismo.dedup/base.z3/snp__ghcb__proto_page.141.smt2 | 550 | 688 | 90 | 100 | 1.45349 | 98.5465 | 0 | 0 |\n", - "| 33 | data/projs/verismo.dedup/base.z3/vbox__vbox.4.smt2 | 426 | 491 | 12 | 99.2958 | 1.62933 | 93.279 | 5.09165 | 0 |\n", - "| 34 | data/projs/verismo.dedup/base.z3/vbox__vbox.5.smt2 | 454 | 583 | 21 | 99.5595 | 1.02916 | 98.6278 | 0.343053 | 0 |\n", - "| 35 | data/projs/vsystemsnew/base.z3/mimalloc-smt-commit_segment.1.smt2 | 73 | 120 | 39 | 97.2603 | 6.66667 | 80.8333 | 0.833333 | 11.6667 |\n", - "| 36 | data/projs/vsystemsnew/base.z3/mimalloc-smt-config.35.smt2 | 13 | 19 | 1 | 100 | 0 | 84.2105 | 0 | 15.7895 |\n", - "| 37 | data/projs/vsystemsnew/base.z3/mimalloc-smt-page_organization__PageOrg.69.smt2 | 194 | 301 | 22 | 98.9691 | 1.99336 | 84.0532 | 13.6213 | 0.332226 |\n", - "| 38 | data/projs/vsystemsnew/base.z3/mimalloc-smt-segment__segment_os_alloc.smt2 | 425 | 495 | 90 | 98.5882 | 2.42424 | 93.9394 | 3.63636 | 0 |\n", - "| 39 | data/projs/vsystemsnew/base.z3/mimalloc-smt-segment__segment_span_free_coalesce_before.smt2 | 664 | 835 | 6 | 97.4398 | 5.50898 | 54.9701 | 39.521 | 0 |\n", - "| 40 | data/projs/vsystemsnew/base.z3/mimalloc-smt-segment__span_queue_delete.smt2 | 643 | 799 | 4 | 96.5785 | 3.00375 | 92.4906 | 4.50563 | 0 |\n", - "| 41 | data/projs/vsystemsnew/base.z3/noderep-smt-spec__cyclicbuffer.3.smt2 | 26 | 21 | 0 | 65.3846 | 0 | 100 | 0 | 0 |\n", - "| 42 | data/projs/vsystemsnew/base.z3/noderep-smt-spec__cyclicbuffer.5.smt2 | 14 | 19 | 0 | 92.8571 | 0 | 78.9474 | 0 | 21.0526 |\n", - "| 43 | data/projs/vsystemsnew/base.z3/page-table-smt-impl_u__l2_refinement.3.smt2 | 287 | 428 | 4 | 98.6063 | 2.1028 | 84.3458 | 0 | 13.5514 |\n", - "| 44 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.10.smt2 | 90 | 129 | 14 | 100 | 0 | 96.124 | 0 | 3.87597 |\n", - "| 45 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.12.smt2 | 180 | 243 | 6 | 91.1111 | 0.823045 | 98.3539 | 0 | 0.823045 |\n", - "| 46 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.13.smt2 | 192 | 258 | 2 | 89.5833 | 0.775194 | 98.4496 | 0 | 0.775194 |\n", - "| 47 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.14.smt2 | 189 | 254 | 28 | 91.0053 | 0.787402 | 96.4567 | 0 | 2.75591 |\n", - "| 48 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.17.smt2 | 129 | 159 | 6 | 86.0465 | 0 | 96.8553 | 0 | 3.14465 |\n", - "| 49 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.2.smt2 | 156 | 200 | 6 | 89.1026 | 0 | 96.5 | 0 | 3.5 |\n", - "| 50 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.4.smt2 | 181 | 264 | 2 | 92.8177 | 0 | 97.3485 | 0 | 2.65152 |\n", - "| 51 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.5.smt2 | 137 | 188 | 18 | 92.7007 | 0 | 95.2128 | 0 | 4.78723 |\n", - "| 52 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__layout_v.30.smt2 | 143 | 210 | 6 | 98.6014 | 0.952381 | 95.7143 | 0 | 3.33333 |\n", - "| 53 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.6.smt2 | 262 | 357 | 7 | 91.6031 | 5.04202 | 92.1569 | 0 | 2.80112 |\n", - "| 54 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.11.smt2 | 184 | 210 | 8 | 89.6739 | 0 | 97.619 | 0 | 2.38095 |\n", - "| 55 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.13.smt2 | 191 | 210 | 7 | 90.0524 | 0 | 99.0476 | 0 | 0.952381 |\n", - "| 56 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.14.smt2 | 201 | 217 | 1 | 90.5473 | 0 | 98.6175 | 0 | 1.38249 |\n", - "| 57 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.15.smt2 | 200 | 227 | 6 | 89 | 0 | 97.7974 | 0 | 2.20264 |\n", - "| 58 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.16.smt2 | 157 | 206 | 7 | 87.8981 | 0 | 95.6311 | 0 | 4.36893 |\n", - "| 59 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.17.smt2 | 146 | 197 | 8 | 90.411 | 0 | 93.9086 | 0 | 6.09137 |\n", - "| 60 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.2.smt2 | 171 | 226 | 7 | 92.3977 | 0 | 97.7876 | 0 | 2.21239 |\n", - "| 61 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.7.smt2 | 140 | 185 | 9 | 94.2857 | 0 | 95.1351 | 0 | 4.86486 |\n", - "| 62 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.9.smt2 | 110 | 137 | 8 | 91.8182 | 0 | 95.6204 | 0 | 4.37956 |\n", - "| 63 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__setup_v.5.smt2 | 175 | 244 | 6 | 88.5714 | 1.63934 | 86.0656 | 0 | 12.2951 |\n", - "| 64 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__setup_v.6.smt2 | 170 | 235 | 7 | 86.4706 | 1.70213 | 85.9574 | 0 | 12.3404 |\n", - "| 65 | data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__start_v.2.smt2 | 231 | 339 | 7 | 93.9394 | 2.94985 | 94.3953 | 0 | 2.65487 |\n", - "+----+------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------+---------------+----------------+--------------------+--------------------+--------------+-------------+----------------+----------------+\n" - ] - } - ], + "outputs": [], "source": [ "df[\"quants_test_rate\"] = df[\"tested_quants\"] / df[\"root_quants\"] * 100\n", "df.drop(\"tested_quants\", axis=1, inplace=True)\n", diff --git a/src/demo_debugger.py b/src/demo_debugger.py index edce930f..28471c99 100644 --- a/src/demo_debugger.py +++ b/src/demo_debugger.py @@ -69,6 +69,7 @@ def check_stabilized(dbg: Debugger3, fa: ExperAnalyzer): fa = ExperAnalyzer(e_filter, QA) df = pd.DataFrame(dbg.editor.get_report()) +dbg.create_singleton_project() df.to_csv("report.csv") # check_tested(dbg, ba) -# check_stabilized(dbg, fa) +check_stabilized(dbg, fa) diff --git a/src/demo_proof.ipynb b/src/demo_proof.ipynb new file mode 100644 index 00000000..30022ed9 --- /dev/null +++ b/src/demo_proof.ipynb @@ -0,0 +1,141 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 4, + "metadata": {}, + "outputs": [ + { + "name": "stderr", + "output_type": "stream", + "text": [ + "\u001b[94m[DEBUG] [term graph] 64997 nodes, 234175 edges, root @[h!392b5117] \u001b[0m\n", + "\u001b[94m[DEBUG] 41 nodes are unreachable! \u001b[0m\n" + ] + }, + { + "ename": "KeyboardInterrupt", + "evalue": "", + "output_type": "error", + "traceback": [ + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mKeyboardInterrupt\u001b[0m Traceback (most recent call last)", + "Cell \u001b[0;32mIn[4], line 24\u001b[0m\n\u001b[1;32m 20\u001b[0m \u001b[38;5;28;01mfrom\u001b[39;00m\u001b[38;5;250m \u001b[39m\u001b[38;5;21;01mdebugger\u001b[39;00m\u001b[38;5;21;01m.\u001b[39;00m\u001b[38;5;21;01mproof_analyzer\u001b[39;00m\u001b[38;5;250m \u001b[39m\u001b[38;5;28;01mimport\u001b[39;00m ProofAnalyzer\n\u001b[1;32m 22\u001b[0m os\u001b[38;5;241m.\u001b[39mchdir(\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124m/home/amarshah/mariposa_fixed/mariposa/\u001b[39m\u001b[38;5;124m\"\u001b[39m)\n\u001b[0;32m---> 24\u001b[0m p \u001b[38;5;241m=\u001b[39m \u001b[43mProofAnalyzer\u001b[49m\u001b[43m(\u001b[49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[38;5;124;43mdbg/199ba4594c/proofs/reseed.3199813507728074554.proof\u001b[39;49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[43m)\u001b[49m\n", + "File \u001b[0;32m~/mariposa_fixed/mariposa/src/debugger/proof_analyzer.py:78\u001b[0m, in \u001b[0;36mProofAnalyzer.__init__\u001b[0;34m(self, file_path)\u001b[0m\n\u001b[1;32m 75\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39m__insts_under_qname: Dict[\u001b[38;5;28mstr\u001b[39m, QuantInstInfo] \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mdict\u001b[39m()\n\u001b[1;32m 77\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mproof_graph \u001b[38;5;241m=\u001b[39m nx\u001b[38;5;241m.\u001b[39mDiGraph()\n\u001b[0;32m---> 78\u001b[0m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43m__analyze_proof_nodes\u001b[49m\u001b[43m(\u001b[49m\u001b[43m)\u001b[49m\n", + "File \u001b[0;32m~/mariposa_fixed/mariposa/src/debugger/proof_analyzer.py:88\u001b[0m, in \u001b[0;36mProofAnalyzer.__analyze_proof_nodes\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 86\u001b[0m \u001b[38;5;28;01mcontinue\u001b[39;00m\n\u001b[1;32m 87\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mproof_graph\u001b[38;5;241m.\u001b[39madd_node(ref)\n\u001b[0;32m---> 88\u001b[0m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43m__analyze_proof_node\u001b[49m\u001b[43m(\u001b[49m\u001b[43mref\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mnode\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 90\u001b[0m \u001b[38;5;66;03m# root will likely be unit-resolution...\u001b[39;00m\n\u001b[1;32m 91\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mproof_graph\u001b[38;5;241m.\u001b[39madd_node(\u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mroot_ref)\n", + "File \u001b[0;32m~/mariposa_fixed/mariposa/src/debugger/proof_analyzer.py:115\u001b[0m, in \u001b[0;36mProofAnalyzer.__analyze_proof_node\u001b[0;34m(self, ref, node)\u001b[0m\n\u001b[1;32m 111\u001b[0m \u001b[38;5;28;01massert\u001b[39;00m name \u001b[38;5;129;01min\u001b[39;00m PROOF_GRAPH_RULES\n\u001b[1;32m 113\u001b[0m conclusion \u001b[38;5;241m=\u001b[39m node\u001b[38;5;241m.\u001b[39mchildren[\u001b[38;5;241m-\u001b[39m\u001b[38;5;241m1\u001b[39m]\n\u001b[0;32m--> 115\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;129;01mnot\u001b[39;00m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mis_proof_free\u001b[49m\u001b[43m(\u001b[49m\u001b[43mconclusion\u001b[49m\u001b[43m)\u001b[49m:\n\u001b[1;32m 116\u001b[0m log_warn(\u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mproof node conclusion is not grounded: \u001b[39m\u001b[38;5;132;01m{\u001b[39;00mref\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m\"\u001b[39m)\n\u001b[1;32m 117\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m\n", + "File \u001b[0;32m~/mariposa_fixed/mariposa/src/debugger/symbol_table.py:272\u001b[0m, in \u001b[0;36mTermTable.is_proof_free\u001b[0;34m(self, ron)\u001b[0m\n\u001b[1;32m 270\u001b[0m \u001b[38;5;28;01mwhile\u001b[39;00m refs:\n\u001b[1;32m 271\u001b[0m node \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mlookup_node(refs\u001b[38;5;241m.\u001b[39mpop())\n\u001b[0;32m--> 272\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28;43misinstance\u001b[39;49m\u001b[43m(\u001b[49m\u001b[43mnode\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mProofNode\u001b[49m\u001b[43m)\u001b[49m:\n\u001b[1;32m 273\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m \u001b[38;5;28;01mFalse\u001b[39;00m\n\u001b[1;32m 274\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28misinstance\u001b[39m(node, AppNode):\n", + "\u001b[0;31mKeyboardInterrupt\u001b[0m: " + ] + } + ], + "source": [ + "import json\n", + "import os, sys\n", + "from tabulate import tabulate\n", + "from tqdm import tqdm\n", + "import pandas as pd\n", + "from z3 import set_param\n", + "\n", + "from base.exper_analyzer import ExperAnalyzer\n", + "from debugger.edit_info import EditAction\n", + "from debugger.informed_editor import InformedEditor\n", + "from debugger.mutant_info import MutantInfo\n", + "\n", + "from debugger3 import Debugger3\n", + "from utils.system_utils import log_info\n", + "from benchmark_consts import *\n", + "from debugger.file_builder import FileBuilder\n", + "from utils.analysis_utils import fmt_percent\n", + "from analysis.singleton_analyzer import SingletonAnalyzer\n", + "\n", + "from debugger.proof_analyzer import ProofAnalyzer\n", + "\n", + "os.chdir(\"/home/amarshah/mariposa_fixed/mariposa/\")\n", + "\n", + "p = ProofAnalyzer(\"dbg/199ba4594c/proofs/reseed.3199813507728074554.proof\")\n", + "\n", + "\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "interesting_qid = \"internal_fluent_controller__kubernetes_api_objects__error__APIError_unbox_axiom_definition\"\n", + "\n", + "# graph = proof_graph(p)\n", + "\n", + "p.debug()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "p.pprint_node(p.lookup_node(\"f440d4ea\"))\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "qref = list(p.quant_names[\"mariposa_qid_63\"])[0]\n", + "p.pprint_node(p.lookup_node(qref))" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "info = p.get_inst_info_under_qname(\"mariposa_qid_63\")\n", + "\n", + "insts = info.get_all_insts()\n", + "print(len(insts))\n", + "\n", + "# p.pprint_node(insts[0], depth = 100)\n", + "\n", + "\n", + "for key in p.neighbors(insts[0]):\n", + " p.pprint_node(key, depth = 3)\n", + " " + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.8.10" + } + }, + "nbformat": 4, + "nbformat_minor": 2 +} diff --git a/src/demo_proof.py b/src/demo_proof.py new file mode 100644 index 00000000..64abf29e --- /dev/null +++ b/src/demo_proof.py @@ -0,0 +1,24 @@ +import json +import os, sys +from tabulate import tabulate +from tqdm import tqdm +import pandas as pd +from z3 import set_param + +from base.exper_analyzer import ExperAnalyzer +from debugger.edit_info import EditAction +from debugger.informed_editor import InformedEditor +from debugger.mutant_info import MutantInfo +from debugger3 import Debugger3 +from utils.system_utils import log_info +from benchmark_consts import * +from debugger.file_builder import FileBuilder +from utils.analysis_utils import fmt_percent +from analysis.singleton_analyzer import SingletonAnalyzer + +from debugger.proof_analyzer import ProofAnalyzer + + + +p = ProofAnalyzer.from_proof_file("dbg/199ba4594c/proofs/reseed.3199813507728074554.proof") + diff --git a/src/files.txt b/src/files.txt new file mode 100644 index 00000000..95832ce1 --- /dev/null +++ b/src/files.txt @@ -0,0 +1,70 @@ +data/projs/flowcert/base.z3/permission.14.smt2 +data/projs/splinterdb/base.z3/allocation_layer__LikesBetree_v__LikesBetree.3.smt2 +data/projs/splinterdb/base.z3/allocation_layer__LikesBetree_v.18.smt2 +data/projs/anvil/base.z3/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof__lemma_eventually_always_no_delete_resource_request_msg_in_flight.smt2 +data/projs/anvil/base.z3/zookeeper-smt-zookeeper_controller__proof__helper_invariants__validation.3.smt2 +data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__stateful_set_match__lemma_from_after_get_stateful_set_step_to_after_update_stateful_set_step.smt2 +data/projs/anvil/base.z3/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof.2.smt2 +data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit__proof__helper_invariants__validation.3.smt2 +data/projs/anvil/base.z3/zookeeper-smt-zookeeper_controller__proof__helper_invariants__zookeeper_api__lemma_zk_request_implies_step_helper.smt2 +data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit__proof__liveness__resource_match__lemma_from_after_get_resource_step_to_after_update_resource_step.smt2 +data/projs/anvil/base.z3/zookeeper-smt-zookeeper_controller__proof__liveness__stateful_set_match.2.smt2 +data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__resource_match.6.smt2 +data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__proof__lemma_eventually_always_every_resource_create_request_implies_at_after_create_resource_step.smt2 +data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit__proof__liveness__daemon_set_match__lemma_from_after_get_daemon_set_step_to_after_update_daemon_set_step.smt2 +data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__resource_match__lemma_from_after_get_resource_step_to_after_update_resource_step.smt2 +data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__resource_match__lemma_from_after_get_resource_step_to_after_create_resource_step.smt2 +data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__resource_match.1.smt2 +data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__proof__lemma_eventually_always_object_in_response_at_after_create_resource_step_is_same_as_etcd.smt2 +data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__liveness__stateful_set_match__lemma_stateful_set_state_matches_at_after_update_stateful_set_step.smt2 +data/projs/anvil/base.z3/zookeeper-smt-rabbitmq-smt-rabbitmq_controller__proof__helper_invariants__validation__lemma_always_stateful_set_in_create_request_msg_satisfies_unchangeable.smt2 +data/projs/anvil/base.z3/zookeeper-smt-zookeeper_controller__proof__helper_invariants__proof__lemma_always_no_update_status_request_msg_in_flight_of_except_stateful_set.smt2 +data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit_config__proof__liveness__resource_match.5.smt2 +data/projs/anvil/base.z3/fluent-smt-fluent_controller__fluentbit__proof__helper_invariants__proof.9.smt2 +data/projs/verismo.dedup/base.z3/boot__init__e820_init.2.smt2 +data/projs/verismo.dedup/base.z3/security__monitor.21.smt2 +data/projs/verismo.dedup/base.z3/vbox__vbox.5.smt2 +data/projs/verismo.dedup/base.z3/arch__ptram__ptram_p2.smt2 +data/projs/verismo.dedup/base.z3/bsp__ap.3.smt2 +data/projs/verismo.dedup/base.z3/snp__cpuid.17.smt2 +data/projs/verismo.dedup/base.z3/snp__ghcb__proto_page.141.smt2 +data/projs/verismo.dedup/base.z3/pgtable_e__pte.20.smt2 +data/projs/verismo.dedup/base.z3/vbox__vbox.4.smt2 +data/projs/verismo.dedup/base.z3/boot__init__e820_init_alloc.1.smt2 +data/projs/verismo.dedup/base.z3/allocator__linkedlist.10.smt2 +data/projs/verismo.dedup/base.z3/pgtable_e__pte.18.smt2 +data/projs/verismo.dedup/base.z3/boot__init__e820_init.4.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.13.smt2 +data/projs/vsystemsnew/base.z3/mimalloc-smt-segment__span_queue_delete.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__setup_v.5.smt2 +data/projs/vsystemsnew/base.z3/mimalloc-smt-commit_segment.1.smt2 +data/projs/vsystemsnew/base.z3/page-table-smt-impl_u__l2_refinement.3.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.17.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.12.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.16.smt2 +data/projs/vsystemsnew/base.z3/mimalloc-smt-config.35.smt2 +data/projs/vsystemsnew/base.z3/noderep-smt-spec__cyclicbuffer.5.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.2.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__logimpl_v.6.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.5.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__start_v.2.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.14.smt2 +data/projs/vsystemsnew/base.z3/page-table-smt-impl_u__l2_refinement.4.smt2 +data/projs/vsystemsnew/base.z3/mimalloc-smt-page_organization__PageOrg.69.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.17.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__setup_v.6.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.11.smt2 +data/projs/vsystemsnew/base.z3/mimalloc-smt-segment__segment_os_alloc.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.7.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.4.smt2 +data/projs/vsystemsnew/base.z3/mimalloc-smt-page_organization__PageOrg__impl_%4__merge_with_before_ll_inv_valid_unused.smt2 +data/projs/vsystemsnew/base.z3/mimalloc-smt-segment__segment_span_free_coalesce_before.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.15.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.9.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.2.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.13.smt2 +data/projs/vsystemsnew/base.z3/noderep-smt-spec__cyclicbuffer.3.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__inv_v.10.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-multilog__inv_v.14.smt2 +data/projs/vsystemsnew/base.z3/verified-storage-smt-verified-storage-smt-storage-node-log__layout_v.30.smt2 +data/projs/atmosphere/base.z3/kernel__create_and_share_pages.5.smt2 \ No newline at end of file diff --git a/src/split_projs.py b/src/split_projs.py new file mode 100644 index 00000000..61473811 --- /dev/null +++ b/src/split_projs.py @@ -0,0 +1,30 @@ +from utils.system_utils import get_name_hash +from splitter import split_query +import os + +file_path = "files.txt" +new_folder_name = "../split_queries" + +os.makedirs(new_folder_name, exist_ok=True) + + +# Open the file and iterate through its lines +with open(file_path, "r") as file: + total_files = 0 + for line in file: + file_name = line.strip() + print(file_name) + print(get_name_hash(file_name)) # Use strip() to remove trailing newline or whitespace + folder = f"{new_folder_name}/splitter_{get_name_hash(file_name)}" + os.makedirs(folder, exist_ok=True) + + file_path = "../../../yizhou7/mariposa/" + file_name + num_queries = split_query(file_path, folder) + total_files += num_queries + print(f"Total number of files {total_files}") + + + + + + diff --git a/src/splitter.py b/src/splitter.py new file mode 100644 index 00000000..6f674842 --- /dev/null +++ b/src/splitter.py @@ -0,0 +1,91 @@ +<<<<<<< HEAD +dir = "data/projs/v_systems/base.z3" +# queries = ["noderep--spec__cyclicbuffer.3.smt2", +# "mimalloc--page_organization__PageOrg__impl__4__take_page_from_unused_queue_ll_inv_valid_unused.smt2", +# "mimalloc--commit_segment.1.smt2", +# "mimalloc--page_organization__PageOrg.69.smt2", +# "noderep--spec__cyclicbuffer.5.smt2", +# "mimalloc--page_organization__PageOrg__impl__4__merge_with_before_ll_inv_valid_unused.smt2", +# "mimalloc--segment__span_queue_delete.smt2"] + +# queries = [ +# "mimalloc--segment__segment_span_free.smt2", +# "mimalloc--segment__segment_span_free_coalesce_before.smt2", +# "mimalloc--queues__page_queue_push_back.smt2", +# "mimalloc--linked_list.25.smt2", +# "mimalloc--segment.1.smt2", +# "mimalloc--queues__page_queue_remove.smt2", +# "mimalloc--page_organization__PageOrg__impl__4__ucount_sum_eq0_inverse.1.smt2" +# ] + +======= +>>>>>>> 921536f60cfdb137eb4302d745dac1ca3216fe74 +import re +import os +import argparse + +def find_largest_location_label_number(file_path): + # Regular expression to match "%%location_label%%" followed by a number + pattern = re.compile(r"%%location_label%%\s*(\d+)") + + max_number = None + + # Open and read the file line by line + with open(file_path, 'r') as file: + for line in file: + # Find all matches in the line + matches = pattern.findall(line) + # Convert found matches to integers and update max_number + for match in matches: + number = int(match) + if max_number is None or number > max_number: + max_number = number + + return max_number + +def add_assertions_to_new_file(file_name, new_folder_name, line_offset, i, n): + # Read the contents of the original file into a list of lines + with open(file_name, 'r') as file: + lines = file.readlines() + + # Generate the new lines based on the given condition + new_lines = [f"(assert (not %%location_label%%{j}))\n" for j in range(n+1) if j != i] + + # Insert the new lines between the third-last and second-last lines + insert_position = len(lines) - line_offset + modified_lines = lines[:insert_position] + new_lines + lines[insert_position:] + + # Derive the new file name by trimming the last 5 characters from the original file name + base_name = os.path.splitext(file_name)[0].split("/")[-1] + new_file_path = f"{new_folder_name}/{base_name}_{i}.smt2" + + os.makedirs(new_folder_name, exist_ok=True) + + # Write the modified lines to the new file + with open(new_file_path, 'w') as new_file: + new_file.writelines(modified_lines) + + print(f"New file created: {new_file_path}") + +# Example usage +line_offset = 1 +def split_query(input_file, output_folder): + largest_number = find_largest_location_label_number(input_file) + for i in range(largest_number + 1): + add_assertions_to_new_file(input_file, output_folder, line_offset, i, largest_number) + + return largest_number + 1 + + + +def main(): + parser = argparse.ArgumentParser(description="Example Python script with a main function") + parser.add_argument("--input", type=str, help="Input File") + parser.add_argument("--output", type=str, help="Output File") + args = parser.parse_args() + + split_query(args.input, args.output) + + +if __name__ == "__main__": + main() \ No newline at end of file