diff --git a/spec/perf-analysis.md b/spec/perf-analysis.md new file mode 100644 index 000000000..ae1a14df0 --- /dev/null +++ b/spec/perf-analysis.md @@ -0,0 +1,213 @@ +# Analysis Report: theory_nseq Improvements Based on ZIPT + +## Overview + +We profiled 3 benchmarks where `theory_nseq` performs worse than both `theory_seq` and ZIPT, +representing the two distinct failure modes observed across the full 54-benchmark suite. + +**Profiled benchmarks:** + +| Benchmark | seq | nseq | ZIPT | Failure Mode | +|-----------|-----|------|------|--------------| +| automatark-lu/instance00000.smt2 | sat (0.32s) | timeout (10s) | sat (fast) | DFS explosion | +| queries/query2885.smt2 | sat (3.1s) | unknown (0.15s) | sat (fast) | Incomplete — gives up | +| hornstr-equiv/Burns_lstar.smt2 | sat (0.38s) | unknown (0.06s) | sat (fast) | Incomplete — gives up | + +Trace files are saved in `spec/traces/`: +- `nseq_automatark_trace.log`, `seq_automatark_trace.log`, `zipt_automatark.log` +- `nseq_query2885_trace.log`, `seq_query2885_trace.log`, `zipt_query2885.log` +- `nseq_burns_trace.log`, `seq_burns_trace.log`, `zipt_burns.log` + +--- + +## Failure Mode 1: DFS Explosion on Regex Bounded Repetitions + +**Affected:** automatark-lu benchmarks (3/54), PCP benchmarks (6/54) + +### Problem + +The automatark benchmark asserts `not (str.in_re X R)` where R uses `(_ re.loop 2 2)`, +`(_ re.loop 4 4)`, and `(_ re.loop 22 22)` over digit ranges. nseq converts this to +membership in `complement(R)` and attempts DFS solving. + +**nseq statistics:** +``` +nseq-dfs-nodes 52,696,075 ← 52M nodes explored before timeout +nseq-final-checks 1 +nseq-solve-calls 1 +``` + +The iterative-deepening DFS in `seq_nielsen.cpp` branches on every character position +using `apply_regex_var_split`, which generates branches for each minterm of the regex +derivative. For bounded repetitions like `(_ re.loop 4 4) (re.range "0" "9")`, this +creates 10 branches per position × 4 positions = 10,000+ paths per loop, and the +benchmark has 5 such loops plus a 22-character alternative. + +### How seq solves it (0.32s) + +theory_seq uses axiom-based regex unfolding via `seq_regex::propagate_in_re`: +- Converts `str.in_re` to `aut.accept` predicates +- Unfolds one character at a time using derivative axioms +- Relies on CDCL(T) conflict-driven learning to prune the search space +- Statistics: 79 axioms, 21 reductions, 9 conflicts, 5 final-checks + +### How ZIPT solves it (fast) + +ZIPT evaluates the regex membership constraint directly at the Boolean level: +``` +Fixed (reMember X!0 (concat ...)): False ← membership determined in one step +``` +ZIPT propagates the Boolean value of `str.in_re` as a fixed assignment, then +finds a satisfying assignment for X (empty string works since the constraint is negated). +No character-by-character enumeration needed. + +### Recommendation + +1. **Add regex membership pre-evaluation**: Before DFS, check if the regex membership + can be evaluated directly (e.g., by finding a witness string using BFS on the regex + automaton, or checking if empty string satisfies). This is what ZIPT does. + +2. **Add DFS node budget with fallback**: When `nseq-dfs-nodes` exceeds a threshold + (e.g., 1M), abandon DFS and fall back to axiom-based unfolding. Currently nseq + runs until timeout. + +3. **Optimize bounded repetition handling**: For `(_ re.loop n n) R`, expand to + length constraint `len(s) = n` + character membership constraints rather than + branching on all `|R|^n` possibilities. + +--- + +## Failure Mode 2: Incomplete — Gives Up on Complex Regex Memberships + +**Affected:** queries (8/54), hornstr-equiv (1/54), slog (1/54), matching (1/54) + +### Problem + +nseq explores only 1 DFS node and returns `unknown` for benchmarks with complex regex +membership constraints. The trace shows: + +**query2885 (Boolean combination of regex memberships):** +``` +nseq populate: 0 eqs, 3 mems -> nielsen root with 0 eqs, 3 mems +nseq length lemma: (>= (str.len x) 6) +nseq length propagation: (>= (str.len x) 6) +Could not match (RegEx String) and (Seq k!0) ← sort mismatch, processing stops +``` + +**Burns (multiple variables with regex + equality):** +``` +nseq populate: 0 eqs, 4 mems -> nielsen root with 0 eqs, 4 mems +nseq length lemma: (>= (str.len varin) 2) +Could not match (RegEx String) and (Seq k!0) ← same issue +``` + +nseq has **0 word equations** and only regex membership constraints. After adding one +length lemma, the DFS finds a single node with no applicable modifiers and gives up. + +The `"Could not match (RegEx String) and (Seq k!0)"` message from `seq_decl_plugin.cpp:74` +indicates a sort-unification failure when nseq tries to process regex constraints through +generic sequence operations. This suggests the regex-to-Nielsen integration has gaps. + +### How seq solves these + +theory_seq uses `seq_regex::propagate_in_re` → `aut.accept` axioms → derivative unfolding: + +**query2885:** 1303 axioms, 1162 reductions → sat in 3.1s +**Burns:** 121 axioms, 22 reductions → sat in 0.38s + +The axiom-based approach systematically unfolds regex memberships through the CDCL(T) +framework, generating constraints one character position at a time. + +### How ZIPT solves these + +ZIPT evaluates multiple regex memberships and propagates their Boolean values: + +**query2885:** +``` +Fixed (reMember x!0 ...): False ← first membership +Fixed (reMember x!0 ...): True ← second membership +Fixed (reMember x!0 ...): False ← third membership +→ SAT (model: x = "\x00\x00\x00ACA") +``` + +**Burns:** +``` +Fixed (reMember varout!0 ...): True +Fixed (reMember varin!13 ...): True +Fixed (reMember varin!13 ...): True ← second membership on varin +Fixed (reMember varin!13 ...): True ← third membership on varin +→ SAT (model: varin = "66", varout = "") +``` + +ZIPT's key advantage: it evaluates regex membership as a **Boolean decision** using +direct automata/derivative evaluation, and uses Decide/Push for SAT search. It doesn't +attempt to enumerate string characters one-by-one through DFS. + +### Recommendation + +1. **Implement regex membership evaluation via automata**: When nseq encounters + `str.in_re(s, R)` with no word equations, build a small automaton for R and check + satisfiability directly. If sat, extract a witness string. This is ZIPT's core approach. + +2. **Handle multiple memberships via product construction**: For problems like Burns + with multiple `str.in_re` on the same variable, compute the intersection automaton + and check emptiness. ZIPT does this implicitly. + +3. **Fix the sort-matching issue**: The `"Could not match (RegEx String) and (Seq k!0)"` + error in `seq_decl_plugin.cpp:74` causes nseq to bail out early. This should be + investigated as a potential bug in how nseq constructs terms during regex processing. + +4. **Add Boolean-level regex propagation**: Like ZIPT's "Fixed" mechanism, when a regex + membership's truth value can be determined (e.g., by finding a satisfying/violating + string), propagate it as a Boolean assignment rather than trying to encode it in the + Nielsen graph. + +--- + +## Summary: What theory_nseq Needs from ZIPT + +| ZIPT Capability | nseq Status | Priority | +|-----------------|-------------|----------| +| Direct regex membership evaluation (automaton-based) | Missing — nseq uses DFS character enumeration | **High** | +| Boolean-level regex propagation (Fixed/Decide) | Missing — nseq tries to encode in Nielsen graph | **High** | +| Multi-membership intersection | Missing — gives up with 1 DFS node | **High** | +| Bounded repetition optimization | Missing — causes 52M-node DFS explosion | **Medium** | +| DFS node budget / fallback | Missing — runs to timeout | **Medium** | +| Sort-matching fix for regex terms | Bug — `Could not match` error | **Medium** | + +### Priority Implementation Order + +1. **Regex membership evaluation** — Direct automaton-based satisfiability check for + `str.in_re` constraints. This single change would fix both failure modes: the DFS + explosion (by avoiding DFS entirely for regex-only problems) and the incompleteness + (by providing an alternative solving path when DFS gives up). + +2. **Boolean-level propagation** — When regex membership is determined, propagate the + result as a Boolean literal rather than encoding in the Nielsen graph. This matches + ZIPT's architecture and works well with the CDCL(T) framework. + +3. **DFS budget with axiom fallback** — For cases where DFS is still used, add a node + budget and fall back to seq-style axiom unfolding when exceeded. + +--- + +## Additional Findings + +### Potential Soundness Bug + +Benchmark #12 (`dining-cryptographers_sat_non_incre_equiv_init_0_3.smt2`): +- seq = **sat**, nseq = **unsat**, ZIPT = **sat** +- nseq reports unsat while the other two agree on sat. This should be investigated + as a potential soundness bug in theory_nseq. + +### nseq Strengths + +nseq excels on word equation problems (track02, track03) and string disequality +(negated-predicates/diseq), solving 6 benchmarks that seq times out on. The Nielsen +transformation approach is fundamentally stronger for these constraint classes. + +### Overall Statistics + +- **Solved**: seq=30, nseq=22, ZIPT=35 (of 54) +- The 13-benchmark gap between nseq and ZIPT is almost entirely due to regex membership + handling (10 benchmarks from queries/hornstr-equiv/slog categories). diff --git a/spec/perf-plan.md b/spec/perf-plan.md new file mode 100644 index 000000000..d5404e8bd --- /dev/null +++ b/spec/perf-plan.md @@ -0,0 +1,32 @@ +\# This is a specification for evaluating and improving theory\_nseq. + +. Build a debug version of z3 in the z3\\build directory + +. Build a release version of z3 in the z3\\release directory + +. To use zipt run .\\ZIPT\\bin\\Debug\\net8.0\\ZIPT.exe -v + +. To profile debug theory\_seq use C:\\c3\\build\\z3.exe -T:10 -st -tr:seq + +. To profile debug theory\_nseq use C:\\c3\\build\\z3.exe -T:10 -st smt.seq.solver=nseq -tr:seq + +. QF\_S benchmarks are in C:\\c3\\tests\\non-incremental\\QF\_S + + + +\# Task + + + +. Pick 50 benchmarks from QF\_S + +. Run theory\_seq, theory\_nseq and zipt on each benchmark + +. Create a report with timing information and status (sat/unsat/unknown/bug/crash) + +. Select at most 3 benchmarks where theory\_nseq is worse than either theory\_seq or zipt. + +. profile these benchmarks using debug builds of z3 and zipt in trace mode. Copy .z3-trace files to allow inspection. + +. Use information from the trace files to create a report of what needs to be implemented for theory\_nseq based on zipt. + diff --git a/spec/perf-report.md b/spec/perf-report.md new file mode 100644 index 000000000..0b6d4c53c --- /dev/null +++ b/spec/perf-report.md @@ -0,0 +1,97 @@ +# Performance Report: theory_nseq vs theory_seq vs ZIPT + +## Results Table + +| # | Benchmark | seq | t(s) | nseq | t(s) | zipt | t(s) | Notes | +|---|-----------|-----|------|------|------|------|------|-------| +| 1 | 20230329-automatark-lu/instance00000.smt2 | sat | 0.492 | timeout | 10.099 | sat | 0.460 | nseqseq** **nseq>zipt** | +| 15 | 20250411-negated-predicates/diseq-None-4-5-107.smt2 | timeout | 10.411 | sat | 0.437 | timeout | 10.000 | **nseq>seq** **nseq>zipt** | +| 16 | 20250411-negated-predicates/not-contains-1-4-5-112.smt2 | timeout | 10.445 | unknown | 0.430 | sat | 0.404 | nseqseq** | +| 45 | track02/02_track_4.smt2 | timeout | 10.072 | sat | 0.723 | sat | 6.008 | **nseq>seq** | +| 46 | track02/02_track_7.smt2 | timeout | 10.428 | sat | 0.644 | sat | 2.855 | **nseq>seq** | +| 47 | track03/03_track_1.smt2 | unsat | 0.065 | unsat | 0.080 | unsat | 0.472 | | +| 48 | track03/03_track_144.smt2 | sat | 0.086 | sat | 0.075 | sat | 0.832 | | +| 49 | track03/03_track_19.smt2 | unsat | 0.094 | unsat | 0.077 | unsat | 0.388 | | +| 50 | track03/03_track_54.smt2 | timeout | 10.448 | unsat | 0.482 | unsat | 0.508 | **nseq>seq** | +| 51 | track04/04_track_1.smt2 | sat | 0.067 | sat | 0.062 | sat | 0.367 | | +| 52 | track04/04_track_144.smt2 | unsat | 0.088 | unsat | 0.072 | unsat | 0.515 | | +| 53 | track04/04_track_19.smt2 | unsat | 0.084 | unsat | 0.068 | unsat | 0.467 | | +| 54 | track04/04_track_54.smt2 | sat | 0.085 | sat | 0.084 | sat | 0.462 | | + +## Summary Statistics + +- **Benchmarks solved (sat/unsat)**: seq=30, nseq=22, zipt=35 (out of 54) +- **Total solve time (solved only)**: seq=15.3s, nseq=5.0s, zipt=26.0s +- **nseq wins vs seq**: 6 benchmarks solved by nseq but not seq +- **nseq wins vs zipt**: 2 benchmarks solved by nseq but not zipt +- **nseq loses vs seq**: 14 benchmarks solved by seq but not nseq +- **nseq loses vs zipt**: 15 benchmarks solved by zipt but not nseq + +## Potential Soundness Issues + +- **#12 20250411-hornstr-equiv/dining-cryptographers_sat_non_incre_equiv_init_0_3.smt2**: seq=sat, nseq=unsat, zipt=sat + +## Worst nseq Regressions + +Benchmarks where nseq is worse than both seq and zipt: + +1. **20230329-automatark-lu/instance00000.smt2** seq=sat(0.492s), nseq=timeout(10.099s), zipt=sat(0.46s) +2. **20230329-automatark-lu/instance05331.smt2** seq=sat(0.469s), nseq=timeout(10.083s), zipt=sat(0.496s) +3. **20230329-automatark-lu/instance10662.smt2** seq=unsat(0.511s), nseq=timeout(10.087s), zipt=unsat(0.489s) +4. **queries-no-ree/query3231.smt2** seq=sat(0.444s), nseq=unknown(0.474s), zipt=sat(0.422s) +5. **20250411-hornstr-equiv/Burns_lstar_non_incre_equiv_bad_0_0.smt2** seq=sat(0.123s), nseq=unknown(0.093s), zipt=sat(0.503s) +6. **slog/slog_stranger_3947_sink.smt2** seq=sat(0.218s), nseq=unknown(0.094s), zipt=sat(0.575s) +7. **queries-no-ree/query5519.smt2** seq=sat(0.222s), nseq=unknown(0.09s), zipt=sat(0.418s) +8. **queries/query6481.smt2** seq=sat(0.218s), nseq=unknown(0.069s), zipt=sat(0.433s) +9. **queries/query3664.smt2** seq=sat(0.271s), nseq=unknown(0.072s), zipt=sat(0.424s) +10. **queries/query2885.smt2** seq=sat(0.886s), nseq=unknown(0.093s), zipt=sat(0.386s) + +## nseq Strengths (where nseq beats seq or zipt) + +- **20250411-negated-predicates/diseq-1-3-5-0.smt2**: seq=timeout(10.067s), nseq=sat(0.461s), zipt=timeout(10.0s) +- **20250411-negated-predicates/diseq-None-4-5-107.smt2**: seq=timeout(10.411s), nseq=sat(0.437s), zipt=timeout(10.0s) +- **track02/02_track_1.smt2**: seq=timeout(10.075s), nseq=sat(0.523s), zipt=sat(0.594s) +- **track02/02_track_4.smt2**: seq=timeout(10.072s), nseq=sat(0.723s), zipt=sat(6.008s) +- **track02/02_track_7.smt2**: seq=timeout(10.428s), nseq=sat(0.644s), zipt=sat(2.855s) +- **track03/03_track_54.smt2**: seq=timeout(10.448s), nseq=unsat(0.482s), zipt=unsat(0.508s) \ No newline at end of file diff --git a/spec/perf-results.csv b/spec/perf-results.csv new file mode 100644 index 000000000..acfa15a33 --- /dev/null +++ b/spec/perf-results.csv @@ -0,0 +1,55 @@ +benchmark,full_path,seq_status,seq_time,nseq_status,nseq_time,zipt_status,zipt_time +20230329-automatark-lu/instance00000.smt2,C:\c3\tests\non-incremental\QF_S\20230329-automatark-lu\instance00000.smt2,sat,0.492,timeout,10.099,sat,0.46 +20230329-automatark-lu/instance05331.smt2,C:\c3\tests\non-incremental\QF_S\20230329-automatark-lu\instance05331.smt2,sat,0.469,timeout,10.083,sat,0.496 +20230329-automatark-lu/instance10662.smt2,C:\c3\tests\non-incremental\QF_S\20230329-automatark-lu\instance10662.smt2,unsat,0.511,timeout,10.087,unsat,0.489 +20240318-omark/cloud-service-query-1.smt2,C:\c3\tests\non-incremental\QF_S\20240318-omark\cloud-service-query-1.smt2,sat,7.603,Result: SAT,0.53,sat,1.092 +20240318-omark/lyndon-schuetzenberg-3.smt2,C:\c3\tests\non-incremental\QF_S\20240318-omark\lyndon-schuetzenberg-3.smt2,timeout,10.065,timeout,10.49,timeout,10.41 +20240318-omark/noodles-unsat-5.smt2,C:\c3\tests\non-incremental\QF_S\20240318-omark\noodles-unsat-5.smt2,timeout,10.445,unknown,0.436,sat,0.939 +20250410-matching/sub-matching-sat-1.smt2,C:\c3\tests\non-incremental\QF_S\20250410-matching\sub-matching-sat-1.smt2,timeout,10.074,timeout,10.448,crash,0.781 +20250410-matching/sub-matching-unsat-16.smt2,C:\c3\tests\non-incremental\QF_S\20250410-matching\sub-matching-unsat-16.smt2,timeout,10.472,timeout,10.443,crash,0.808 +20250410-matching/wildcard-matching-regex-104.smt2,C:\c3\tests\non-incremental\QF_S\20250410-matching\wildcard-matching-regex-104.smt2,sat,0.531,unknown,0.085,unknown,0.404 +20250410-matching/wildcard-matching-regex-41.smt2,C:\c3\tests\non-incremental\QF_S\20250410-matching\wildcard-matching-regex-41.smt2,crash,0.389,unknown,0.341,crash,0.699 +20250411-hornstr-equiv/Burns_lstar_non_incre_equiv_bad_0_0.smt2,C:\c3\tests\non-incremental\QF_S\20250411-hornstr-equiv\Burns_lstar_non_incre_equiv_bad_0_0.smt2,sat,0.123,unknown,0.093,sat,0.503 +20250411-hornstr-equiv/dining-cryptographers_sat_non_incre_equiv_init_0_3.smt2,C:\c3\tests\non-incremental\QF_S\20250411-hornstr-equiv\dining-cryptographers_sat_non_incre_equiv_init_0_3.smt2,sat,0.1,Result: UNSAT,0.107,sat,0.488 +20250411-hornstr-equiv/muzzle_sat_non_incre_equiv_bad_0_13.smt2,C:\c3\tests\non-incremental\QF_S\20250411-hornstr-equiv\muzzle_sat_non_incre_equiv_bad_0_13.smt2,unsat,0.059,unsat,0.097,unsat,0.419 +20250411-negated-predicates/diseq-1-3-5-0.smt2,C:\c3\tests\non-incremental\QF_S\20250411-negated-predicates\diseq-1-3-5-0.smt2,timeout,10.067,Result: SAT,0.461,timeout,10 +20250411-negated-predicates/diseq-None-4-5-107.smt2,C:\c3\tests\non-incremental\QF_S\20250411-negated-predicates\diseq-None-4-5-107.smt2,timeout,10.411,Result: SAT,0.437,timeout,10 +20250411-negated-predicates/not-contains-1-4-5-112.smt2,C:\c3\tests\non-incremental\QF_S\20250411-negated-predicates\not-contains-1-4-5-112.smt2,timeout,10.445,unknown,0.43,sat,0.404 +pcp-3-3-random/pcp_instance_0.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-3-random\pcp_instance_0.smt2,unknown,0.098,timeout,10.077,unknown,0.321 +pcp-3-3-random/pcp_instance_248.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-3-random\pcp_instance_248.smt2,unknown,0.462,timeout,10.077,unknown,0.289 +pcp-3-3-random/pcp_instance_398.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-3-random\pcp_instance_398.smt2,unknown,0.456,timeout,10.074,unknown,0.316 +pcp-3-4-hard/unsolved_pcp_instance_0.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-4-hard\unsolved_pcp_instance_0.smt2,unknown,0.467,timeout,10.074,unknown,0.335 +pcp-3-4-hard/unsolved_pcp_instance_248.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-4-hard\unsolved_pcp_instance_248.smt2,unknown,0.458,timeout,10.061,unknown,0.316 +pcp-3-4-hard/unsolved_pcp_instance_398.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-4-hard\unsolved_pcp_instance_398.smt2,unknown,0.468,timeout,10.072,unknown,0.305 +queries/query2885.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries\query2885.smt2,sat,0.886,unknown,0.093,sat,0.386 +queries/query3358.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries\query3358.smt2,sat,0.519,unknown,0.068,sat,0.448 +queries/query3664.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries\query3664.smt2,sat,0.271,unknown,0.072,sat,0.424 +queries/query6481.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries\query6481.smt2,sat,0.218,unknown,0.069,sat,0.433 +queries-no-ree/query10041.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries-no-ree\query10041.smt2,sat,0.798,unknown,0.075,sat,0.448 +queries-no-ree/query3231.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries-no-ree\query3231.smt2,sat,0.444,unknown,0.474,sat,0.422 +queries-no-ree/query3723.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries-no-ree\query3723.smt2,sat,0.422,unknown,0.082,sat,0.451 +queries-no-ree/query5519.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries-no-ree\query5519.smt2,sat,0.222,unknown,0.09,sat,0.418 +rna-sat/benchmark_0001.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-sat\benchmark_0001.smt2,unknown,0.079,unknown,0.06,unknown,0.275 +rna-sat/benchmark_0167.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-sat\benchmark_0167.smt2,unknown,0.074,unknown,0.08,unknown,0.276 +rna-sat/benchmark_0333.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-sat\benchmark_0333.smt2,unknown,0.109,unknown,0.09,unknown,0.269 +rna-unsat/benchmark_0001.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-unsat\benchmark_0001.smt2,unknown,0.08,unknown,0.097,unknown,0.246 +rna-unsat/benchmark_0167.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-unsat\benchmark_0167.smt2,unknown,0.091,unknown,0.088,unknown,0.269 +rna-unsat/benchmark_0333.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-unsat\benchmark_0333.smt2,unknown,0.099,unknown,0.094,unknown,0.293 +slog/slog_stranger_1001_sink.smt2,C:\c3\tests\non-incremental\QF_S\2019-Jiang\slog\slog_stranger_1001_sink.smt2,unsat,0.092,unsat,0.084,unsat,0.416 +slog/slog_stranger_2251_sink.smt2,C:\c3\tests\non-incremental\QF_S\2019-Jiang\slog\slog_stranger_2251_sink.smt2,unsat,0.433,unsat,0.077,unsat,0.352 +slog/slog_stranger_3947_sink.smt2,C:\c3\tests\non-incremental\QF_S\2019-Jiang\slog\slog_stranger_3947_sink.smt2,sat,0.218,unknown,0.094,sat,0.575 +track01/01_track_1.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track01\01_track_1.smt2,sat,0.084,sat,0.082,sat,0.404 +track01/01_track_144.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track01\01_track_144.smt2,sat,0.06,sat,0.094,sat,0.503 +track01/01_track_19.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track01\01_track_19.smt2,sat,0.073,sat,0.061,sat,0.434 +track01/01_track_54.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track01\01_track_54.smt2,sat,0.101,Result: SAT,0.093,sat,1.142 +track02/02_track_1.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track02\02_track_1.smt2,timeout,10.075,Result: SAT,0.523,sat,0.594 +track02/02_track_4.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track02\02_track_4.smt2,timeout,10.072,Result: SAT,0.723,sat,6.008 +track02/02_track_7.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track02\02_track_7.smt2,timeout,10.428,Result: SAT,0.644,sat,2.855 +track03/03_track_1.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track03\03_track_1.smt2,unsat,0.065,unsat,0.08,unsat,0.472 +track03/03_track_144.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track03\03_track_144.smt2,sat,0.086,Result: SAT,0.075,sat,0.832 +track03/03_track_19.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track03\03_track_19.smt2,unsat,0.094,unsat,0.077,unsat,0.388 +track03/03_track_54.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track03\03_track_54.smt2,timeout,10.448,Result: UNSAT,0.482,unsat,0.508 +track04/04_track_1.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track04\04_track_1.smt2,sat,0.067,sat,0.062,sat,0.367 +track04/04_track_144.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track04\04_track_144.smt2,unsat,0.088,unsat,0.072,unsat,0.515 +track04/04_track_19.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track04\04_track_19.smt2,unsat,0.084,unsat,0.068,unsat,0.467 +track04/04_track_54.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track04\04_track_54.smt2,sat,0.085,sat,0.084,sat,0.462