Rounding mode fixes

.clang-tidy

@@ -0,0 +1,74 @@
+# clang-tidy gate config — the type-aware companion to the regex lint.py.
+#
+# Three concerns, all things a regex lint structurally cannot see (they are
+# *semantic*, type-dependent), run via ./copy_lint.sh (incremental by default,
+# --all for a full sweep; it adds --warnings-as-errors and the macOS -isysroot fixup):
+#
+#   1. Accidental by-value COPIES of heavy types (Box, capd::IMap, Environment,
+#      IntervalVector, ...). This solver is memory-bound; a stray copy where a
+#      const& / move belongs is a silent regression. Covered by the performance-*
+#      copy subset (unnecessary-value-param, for-range-copy,
+#      unnecessary-copy-initialization, move-const-arg, implicit-conversion-in-loop).
+#
+#   2. Other PERFORMANCE pitfalls (avoid-endl, inefficient-vector-operation,
+#      noexcept-move, etc.) — the rest of performance-*.
+#
+#   3. UNDEFINED BEHAVIOR / memory-safety / segfault-class bugs — an explicit
+#      allow-list of the bugprone-* checks whose findings are genuine UB or memory
+#      corruption (use-after-move, dangling-handle, undefined-memory-manipulation,
+#      ptr/array mismatches, sizeof misuse, ...). The whole tree is currently clean
+#      on every one of these, so they cost zero noise and exist purely to catch a
+#      future regression. NOT the style/intent bugprone checks (easily-swappable-
+#      parameters, narrowing-conversions, branch-clone, ...) — those are noise here.
+#
+# Findings are resolved by fixing (const& / move / the real bug) or, when genuinely
+# intended, justified inline with // NOLINT(<check>) <reason> — the type-aware twin
+# of lint.py's `// lint: allow`.
+#
+# Two deliberately-excluded checks (see ./copy_lint.sh history):
+#   -performance-enum-size            micro-opt only (smaller enum base); 12 core
+#                                     enums, mild serialization/arithmetic risk, no
+#                                     correctness value.
+#   -bugprone-unchecked-optional-access  crash-class but FP-prone; its only hits are
+#                                     in the semi-dead pattern_matching trie code.
+#
+# No WarningsAsErrors here on purpose: editors/clangd surface these as plain
+# warnings; the hard fail is the gate script's job (copy_lint.sh adds it).
+Checks: >
+  -*,
+  performance-*,
+  -performance-enum-size,
+  bugprone-bitwise-pointer-cast,
+  bugprone-bool-pointer-implicit-conversion,
+  bugprone-casting-through-void,
+  bugprone-dangling-handle,
+  bugprone-dynamic-static-initializers,
+  bugprone-fold-init-type,
+  bugprone-incorrect-roundings,
+  bugprone-invalid-enum-default-initialization,
+  bugprone-misplaced-operator-in-strlen-in-alloc,
+  bugprone-misplaced-pointer-arithmetic-in-alloc,
+  bugprone-misplaced-widening-cast,
+  bugprone-multi-level-implicit-pointer-conversion,
+  bugprone-multiple-new-in-one-expression,
+  bugprone-not-null-terminated-result,
+  bugprone-pointer-arithmetic-on-polymorphic-object,
+  bugprone-raw-memory-call-on-non-trivial-type,
+  bugprone-return-const-ref-from-parameter,
+  bugprone-shared-ptr-array-mismatch,
+  bugprone-signed-char-misuse,
+  bugprone-sizeof-container,
+  bugprone-sizeof-expression,
+  bugprone-string-constructor,
+  bugprone-string-literal-with-embedded-nul,
+  bugprone-stringview-nullptr,
+  bugprone-suspicious-memory-comparison,
+  bugprone-suspicious-memset-usage,
+  bugprone-suspicious-realloc-usage,
+  bugprone-suspicious-stringview-data-usage,
+  bugprone-unhandled-self-assignment,
+  bugprone-undefined-memory-manipulation,
+  bugprone-unique-ptr-array-mismatch,
+  bugprone-unused-raii,
+  bugprone-use-after-move
+HeaderFilterRegex: 'src/dreal/.*'

.claude/skills/benchmark-baseline/skill.md

@@ -6,7 +6,7 @@ description: Re-establish a local performance baseline by running ~30 stratified
 # /benchmark-baseline skill
 
 1. **Confirm with user first:**
-   > This will run ~30 benchmarks (~15-20 min) and update `benchmark/state.json` to use a local baseline. Proceed?
+   > This will run ~70 benchmarks (all 43 odeexpr + ~10 each of saradc/github/tacas, at the 600 s timeout — can take 30-45 min) and update `benchmark/state.json` to use a local baseline. Proceed?
 
    Wait for confirmation before continuing.
 
@@ -15,18 +15,18 @@ description: Re-establish a local performance baseline by running ~30 stratified
 3. Spawn a Haiku subagent with this exact prompt:
 
 ---
-Run the dReal4 baseline script (foreground, 1200000ms timeout):
+Run the dReal4 baseline script (foreground, 1800000ms timeout):
 ```bash
 bash /Users/kunalsheth/Documents/new_dreal/dreal4-cmake/benchmark/do_baseline.sh
 ```
 The script prints OUT_DIR to stdout when done. Use the Read tool to read `<OUT_DIR>/aggregate.json`. Do not run any other commands or read any other files.
 
-The `aggregate.json` contains a `family_comparison` key with per-family frozen vs local averages, and a `baseline_sha` key.
+The `aggregate.json` contains a `family_comparison` key with per-family frozen vs local averages (including a weighted `odeexpr` family and a `weighted_overall` row), and a `baseline_sha` key.
 
 Return a formatted summary as your only output:
-- Header: `Baseline established from <baseline_sha> — <n_ran> benchmarks across 3 families`
-- Table: one row per family from `family_comparison` — family | n | frozen PAR2 avg | local PAR2 avg | ratio (keys: `frozen_avg_par2`, `local_avg_par2`)
-- One sentence: faster/slower/comparable? Flag >20% systematic differences as potentially a build config issue.
+- Header: `Baseline established from <baseline_sha> — <n_ran> benchmarks across 4 families`
+- Table: one row per family from `family_comparison` — family | n | weight | frozen PAR2 avg | local PAR2 avg | ratio (keys: `frozen_avg_par2`, `local_avg_par2`, `weight`), then the `weighted_overall` row last
+- One sentence: faster/slower/comparable? Flag >20% systematic differences as potentially a build config issue. PAR2 is CPU time (user+sys), 600 s timeout.
 - Last line: `baseline_local: benchmark/baseline_local.csv`
 
 Be terse. Only return the final summary — no narration.

.claude/skills/benchmark/skill.md

@@ -10,20 +10,23 @@ description: Run a quick regression benchmark batch (~8-12 benchmarks) for the d
 2. Spawn a Haiku subagent with this exact prompt:
 
 ---
-Run the dReal4 benchmark script (foreground, 420000ms timeout):
+Run the dReal4 benchmark script (foreground, 1500000ms timeout):
 ```bash
 bash /Users/kunalsheth/Documents/new_dreal/dreal4-cmake/benchmark/do_benchmark.sh
 ```
 The script prints OUT_DIR to stdout when done. Use the Read tool to read `<OUT_DIR>/aggregate.json`.
 
 Return a formatted summary as your only output:
 - If `correctness_flips` is non-empty, lead with: **CORRECTNESS REGRESSION**: [names] changed SAT/UNSAT result.
+- Then, if any regression has priority `ODEEXPR-HIGH`/`ODEEXPR` (the high-priority ode_expressivity family — names start `odeexpr_`), lead with those next: **ODEEXPR REGRESSION**: [names]. odeexpr is weighted ~3× the other families, so treat its regressions as more serious and its speedups as more meaningful.
 - First line: `N ran, M regressions, K exceptional`
-- 2–4 sentences: (1) overall health, (2) notable timing changes using PAR2 scores (e.g. "PAR2: 50 s vs 600 s (0.08×, formerly TIM)" for a benchmark that went from timeout to solve), (3) whether exceptional speedups look real or noise
+- 2–4 sentences: (1) overall health, (2) notable timing changes using PAR2 scores — PAR2 is now CPU time (user+sys), 600 s timeout / 1200 s penalty (e.g. "PAR2: 50 s vs 1200 s (0.04×, formerly TIM)"), (3) whether exceptional speedups look real or noise
 - One sentence: what needs investigation before continuing, if anything
 - Last line: `anomaly_report: <OUT_DIR>/anomaly_report.txt`
 
-Be terse. Only return the final summary — no narration.
+Then, as the FINAL part of your output, ALWAYS render the per-family PAR2 table from `family_comparison` in `aggregate.json` (the run vs the frozen baseline, `baseline_sha` in the same file). One markdown table, one row per family plus `weighted_overall`, columns: Family | Weight | n | Baseline PAR2 (s) | This run PAR2 (s) | Ratio. Sort families by descending weight (odeexpr, saradc, tacas, github) with `weighted_overall` last. Flag ratio >1.5 as a regression and <0.6 as exceptional. If `family_comparison` is absent (older run), say so in one line instead of inventing numbers.
+
+Be terse. Only return the final summary + the PAR2 table — no narration.
 
 ---
 

.gitattributes

@@ -0,0 +1,2 @@
+# Binary research papers (docs/papers/) are stored via Git LFS, not as blobs.
+*.pdf filter=lfs diff=lfs merge=lfs -text

.gitignore

@@ -463,7 +463,10 @@ pip-selfcheck.json
 
 .idea
 .idea/**
-smt2
+# top-level SMT2 examples/scratch dir only — anchored so it does NOT match the
+# source dir src/dreal/smt2/ or the test fixtures under test/dreal/test/smt2/.
+/smt2/
 gcc_build
 past_compilations
-benchmark/results/
+benchmark/results/
+dreal_popl27