This updates a formatting regression introduced in the `pop_app_frame`
non-`expr_head` path, where block indentation made control flow harder
to read. The patch is whitespace-only and keeps parser behavior
unchanged.
- **What changed**
- Reindented the `else` body in
`src/parsers/smt2/smt2parser.cpp::pop_app_frame` so nested `if/else`
structure is visually unambiguous.
- Removed trailing spaces on the `m_ctx.mk_app(symbol("select"), ...)`
lines in the same block.
- **Scope**
- No control-flow, data-flow, or API changes.
- No changes outside `pop_app_frame`.
```cpp
// Before
else {
local l;
if (m_env.find(fr->m_f, l)) {
...
}
else {
...
}
}
// After
else {
local l;
if (m_env.find(fr->m_f, l)) {
...
}
else {
...
}
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
So far, `algebraic_numbers compare_core ` handles an edge case
incorrectly:
- If the two compared numbers (`a`, `b`) are different,
- the intervals still overlap after refinements, and
- both a and b are a root of the second polynomial (`cell_b->m_p`), e.g.
they are the first and second root
then the method would return `sign_zero` (i.e. "equal"). This behavior
can be replicated with the provided test case (before the fix). This
requires `algebraic.factor=false`, though i first encountered it during
solver runs on QF_NRA instances with the default
`algebraic.factor=true`, which apparently means that the polynomials for
anums are still not always factored.
The fix is to compare the interval bounds of b to a and vice versa. Then
the Sturm-Tarski check is only run if `a` and `b` both lie in the
intersection of the intervals, because only then is it guaranteed to be
correct.
The SMT2 front-end rejected valid higher-order inputs using `HO_ALL` and
failed on curried applications where the function position is itself an
expression (e.g., `((transfer top) 0)`).
This update adds `HO_ALL` support and makes curried parsing consistently
lower to implicit `select` chains.
- **Logic recognition**
- Treat `HO_ALL` as an `ALL`-class logic in SMT logic classification.
- This unblocks `(set-logic HO_ALL)` in the standard SMT2 command path.
- **Curried application parsing**
- Extend application-frame handling to support parenthesized expression
heads, not only symbol heads.
- When the head is an expression, parse application arguments normally
and construct nested implicit selects:
- `(f a b)` → `(select (select f a) b)`
- Preserve existing behavior for symbol-based applications, qualified
identifiers, and lambda-led forms.
- **Regression coverage**
- Add a focused parser/eval regression using the reported higher-order
case to lock in behavior.
```smt2
(set-logic HO_ALL)
(declare-fun transfer () (-> (-> Int Bool) (-> Int Bool)))
(assert (forall ((P (-> Int Bool))) (=> (P 0) ((transfer P) 0))))
(declare-fun top () (-> Int Bool))
(assert (forall ((x Int)) (top x)))
(assert (not ((transfer top) 0)))
(check-sat)
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Adds a new lemma pattern to nla_grobner::propagate_quotients that
derives a modular-residue constraint from polynomial divisibility,
filling a gap between quotient1-5 (model-value-driven case splits) and
the polynomials Grobner actually produces on Skolem-encoded mod
arithmetic.
Pattern
-------
For a polynomial p with all-integer free variables and a linear monomial
c_v * v (single integer var), the pattern computes M = gcd(|c_i/c_v|)
over the other monomials and K = c0/c_v for the constant term. When both
are integers, dividing p by c_v gives
v + M*Q + K = 0 with Q an integer
so v ≡ -K (mod M). The pattern emits the sound disjunctive lemma
(v < 0) ∨ (v ≥ M) ∨ (v = target)
where target = (-K) mod M ∈ [0, M-1]. This encodes "v ∈ target + M·Z" in
a form the LP / SAT layer can refute against current bounds.
Motivation
----------
QF_UFNIA verification benchmarks over fixed-prime modular arithmetic
(e.g. zk applications using the BabyBear prime 2013265921) regularly
produce basis polynomials of the form
-p*v_div + p*(v_a * v_b) - v_mod = 0
where v_mod is the result of (mod (* v_a v_b) p). The polynomial sits in
the Grobner basis but none of quotient1-5 fires: they all require
specific model-value alignments (r_value == 0, |v_value| > |r_value|,
etc.) that don't hold when all variables in scope are similarly sized
integers in [0, p). The proof spins on interval-tightening lemmas
without ever extracting the modular conclusion.
The author of propagate_quotients flagged this gap with the comment
\"other division lemmas are possible\" preceding the fall-through \"no
lemmas found\" CTRACE. This patch supplies one.
Soundness
---------
The lemma is sound regardless of v's LP bounds — the bound-negation
disjuncts (v < 0) and (v ≥ M) make the disjunction unconditionally true
under the polynomial identity, with v = target as the canonical residue
in [0, M-1]. M is derived from the polynomial's coefficient gcd, not
from any LP-side bound.
Validated under smt.arith.validate=true on the mod-factor-propagation
reproducers (PR #9235 follow-up), zk verifier benchmarks, and a broader
QF_UFNIA sample — 50+ files total, zero validate_conflict() assertion
violations.
Performance
-----------
A model-value gate (skip emission when v's current value already
satisfies one of the disjuncts) prevents the pattern from
short-circuiting the propagate_quotients || propagate_gcd_test ||
propagate_eqs || propagate_factorization || propagate_linear_equations
chain with redundant emissions. Without the gate, a single (v, M,
target) triple can re-emit each Grobner round and starve the downstream
propagators — observed in regression testing as thousands of identical
emissions on a small benchmark, turning a sub-second closure into a
timeout.
On six small mod-factor-propagation reproducers, the patch closes four
cases that previously timed out at 30 s (~1 s typical under the
Grobner-ramped config: smt.arith.nl.gr_q=50,
smt.arith.nl.grobner_eqs_growth=50,
smt.arith.nl.grobner_exp_delay=false, smt.arith.nl.grobner_frequency=1).
The two remaining timeouts in that set are attributable to different
gaps (Boolean-disjunction propagation, and the multi-bounded-mod-result
polynomial shape that needs Grobner over Z/pZ), not to mod_residue
itself.
Diagnostics
-----------
TRACE under the existing 'grobner' tag emits one line per lemma
emission, recording v, M, c_v, c0, and target.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
The JS bindings currently assume the wasm can be located via the default
Emscripten path resolution, which can force Deno users into
`--allow-read`. This change lets callers provide a custom wasm load path
through `init(...)`, so Deno can resolve the packaged wasm asset without
filesystem reads.
- **Public init API**
- Extend the JS entrypoints (`node` and `browser`) so `init(...)`
accepts optional Emscripten module overrides.
- Surface a typed `Z3ModuleOverrides` shape with explicit support for
`locateFile(path, prefix)`.
- **Low-level initialization**
- Thread module overrides through the generated low-level wrapper
instead of always calling the Emscripten module factory with no
arguments.
- Keep the default behavior unchanged when no overrides are provided.
- **Docs**
- Document the Deno usage pattern in the published JS README.
- Clarify the `locateFile` signature and show the intended Deno 2.1+
`import.meta.resolve(...)` flow.
- **Focused coverage**
- Add unit tests for `node` and `browser` init to verify module
overrides are forwarded correctly.
Example:
```ts
import { init } from 'npm:z3-solver';
const api = await init({
locateFile: (file, _prefix): string =>
import.meta.resolve(`npm:z3-solver/build/${file}`),
});
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
The Windows ARM64 nightly build (`mk_win_dist_cmake.py --arm64-only`)
was failing because the cmake-built `Microsoft.Z3` NuGet package was
produced without any native Windows DLL, causing the downstream dotnet
example build to fail.
## Root causes
- **Wrong DLL path in `Microsoft.Z3.csproj.in`**: Path included
`/$(_DN_CMAKE_CONFIG)/` (e.g., `.../RelWithDebInfo/libz3.dll`), but
`CMakeLists.txt` sets `CMAKE_RUNTIME_OUTPUT_DIRECTORY =
PROJECT_BINARY_DIR` with no config subdir. With Ninja single-config, the
DLL lands at `build-dir/libz3.dll`. The `Exists()` guard silently
excluded the DLL from the package.
- **Wrong runtime identifier**: ARM64 DLL was being packed under
`runtimes\win-x64\native` instead of `runtimes\win-arm64\native`.
- **Legacy copy fires for `net8.0`**: `Microsoft.Z3.targets` excluded
`netstandard`/`netcoreapp` but not modern TFMs like `net8.0`, so
`CopyToOutputDirectory` fired and failed trying to copy the absent
`win-x64` DLL.
## Changes
- **`src/api/dotnet/CMakeLists.txt`**: Introduce `Z3_DOTNET_WIN_RID`
cmake variable (`win-x64` / `win-x86` / `win-arm64`) derived from
`TARGET_ARCHITECTURE`; used at `configure_file` time.
- **`src/api/dotnet/Microsoft.Z3.csproj.in`**: Remove
`/$(_DN_CMAKE_CONFIG)` from the Windows DLL path; replace hardcoded
`runtimes\win-x64\native` with `runtimes\${Z3_DOTNET_WIN_RID}\native`.
- **`src/api/dotnet/Microsoft.Z3.targets`**: Add
`!$(TargetFramework.Contains('.'))` to the legacy-copy condition, which
correctly excludes `net5.0`/`net6.0`/`net7.0`/`net8.0` (all use dotted
TFMs) while keeping `net45`/`net472` etc.
- **`src/api/dotnet/Microsoft.Z3.props`**: Add explicit `arm64`
condition mapping `$(Platform) == 'arm64'` to
`runtimes\win-arm64\native\libz3.dll` for legacy .NET Framework ARM64
consumers.
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Z3 could return `sat` for an unsatisfiable QF_ABV formula equating two
store chains over distinct constant arrays. The rewrite path for array
equalities was missing a necessary base-value constraint in
finite-domain cases where stores cannot cover all indices.
- **Root cause**
- In `array_rewriter::mk_eq_core`, equality rewriting for nested stores
over const-array bases did not enforce equality of the underlying const
values when the index domain size exceeds the number of updated indices.
- **Rewriter fix**
- Added a sound rewrite branch for:
- `store* ((as const ...) v)` vs `store* ((as const ...) w)`
- When `|domain| > (#stores_lhs + #stores_rhs)`, rewrite now includes:
- select equalities for touched indices (existing behavior)
- **and** base-value equality `v = w` (new requirement)
- This prevents spurious models where only updated indices are
constrained.
- **Regression coverage**
- Added a focused regression in `src/test/mod_factor.cpp` that asserts
`unsat` for a minimized constant-array/store-chain BV case with
`(distinct x y)` and one store per side.
```cpp
(assert (distinct x y))
(assert (= (store A0 i0 e0) (store A1 i1 e1)))
(check-sat) ; expected: unsat
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Fix the TPTP frontend so that a bare name used in an equality refers to
a single shared `func_decl`, regardless of how the surrounding context
coerces its sort.
## Problem
With the following input the conjecture was not proved:
```tptp
fof(a1,axiom, ! [X] : (X = a)).
fof(c1,conjecture, b = a).
```
`parse_atomic_formula` created bare names as 0-arity **Bool
predicates**, and `coerce_eq` later retyped them by calling
`m.mk_func_decl(...)` directly, without registering the result in
`m_decls`. So the `a` used inside `! [X] : (X = a)` (coerced to sort
`U`) and the `a` used inside `b = a` (left as Bool) ended up as two
unrelated `func_decl`s sharing only the name. The axiom no longer
constrained the conjecture.
## Fix
In `src/cmd_context/tptp_frontend.cpp`:
1. Add `mk_zero_arity_decl(name, range)` / `coerce_zero_arity(app*,
range)` helpers that memoize the 0-arity `func_decl` per `(name, target
sort)` in `m_decls`, delegating to the existing `mk_decl_or_ho_const`
for `U` and Bool targets.
2. Rewrite `coerce_eq` to use the new helpers and add an explicit Bool /
non-Bool retyping branch so a bare-Bool side is recast to the other
side's sort.
3. In `parse_atomic_formula`, when a bare name is immediately followed
by `=` or `!=`, create it as a non-predicate (sort `U`). Terms in
equalities are no longer first introduced as Bool predicates.
4. Reorder the constructor init-list so `m_univ` is initialized before
the pinned ref vectors (matches declaration order; silences
`-Wreorder`).
Net effect: every reference to a given name at a given sort yields the
same `func_decl`, eliminating duplicate-symbol bugs in equalities over
bare TPTP constants.
## Test
Added `fof-bare-constant-equality` to `src/test/tptp.cpp`. Without the
C++ change the new case asserts; with it, `./build/release/test-z3 /seq
tptp` reports `PASS`.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Preserve the de-linearization of the linear constraints but fixing the
den bug. @ValentinPromies, that is what you had in mind.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Spacer can crash on small HORN/ADT benchmarks when model construction
reaches datatype enodes without a fully populated constructor state. The
failure manifested as a null/invalid-path dereference inside datatype
model value generation.
- **Root cause area: datatype model extraction path**
- Hardened `theory_datatype::mk_value` to handle incomplete theory state
safely instead of assuming constructor metadata is always present.
- Added guarded fallback to a factory-provided datatype value when:
- `th_var` is missing,
- union-find lookup is invalid,
- var data/constructor is unavailable.
- **Behavioral change**
- Missing constructor state now degrades to a safe model value
(`expr_wrapper_proc`) instead of crashing during model generation.
- **Regression coverage**
- Added a focused API regression in `src/test/api_datalog.cpp` using a
Spacer + ADT HORN script (with reproducing seed) to ensure the code path
executes without parser/runtime failure.
```cpp
// theory_datatype::mk_value fallback shape
if (v == null_theory_var || invalid_var_data || d->m_constructor == nullptr) {
app* val = to_app(m_factory->get_some_value(n->get_sort()));
return alloc(expr_wrapper_proc, val);
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This change simplifies recently touched API code in
`src/api/api_ast.cpp` without altering semantics. It removes an
unreachable error path in `Z3_get_index_value` and deletes an empty
comment in `Z3_mk_rec_func_decl`.
- **`Z3_get_index_value`: remove dead branch**
- After validating `a` is non-null and of kind `AST_VAR`, the conversion
to `var*` is already guaranteed by existing AST casting invariants.
- The redundant null-check/error-return branch was removed, leaving a
direct index return.
- **`Z3_mk_rec_func_decl`: remove noise**
- Deleted a stray empty `//` line.
```cpp
// before
var* va = to_var(_a);
if (va) {
return va->get_idx();
}
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return 0;
// after
var* va = to_var(_a);
return va->get_idx();
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
`sat.smt=true` could return `sat` with an invalid model for QF_UFBV
formulas combining Bool-valued UFs and BV range constraints. The failure
came from broken model-trail reconstruction in `elim_unconstrained`,
where `ADD` entries were effectively turned into identity substitutions.
- **Root-cause fix: restore model-trail substitution composition**
- In `elim_unconstrained::update_model_trail`,
`generic_model_converter::ADD` entries now use `entry.m_def` (rewritten
through accumulated substitutions) instead of creating self-referential
const-to-const mappings.
- This re-enables correct back-substitution for eliminated unconstrained
terms during witness reconstruction.
- **Regression coverage: QF_UFBV + `sat.smt=true` + model validation**
- Added a focused unit test in `src/test/simplifier.cpp` for:
- Bool-valued UF predicate over BV vars
- split BV range constraints (`bvuge` / `bvult`)
- `:sat.smt true` and `:model_validate true`
- The test asserts the solver returns `sat` without emitting an
invalid-model error.
```cpp
// before (effectively no-op back-mapping)
new_def = m.mk_const(entry.m_f);
sub->insert(new_def, new_def, nullptr, nullptr);
// after (compose and apply recorded definition)
new_def = entry.m_def;
(*rp)(new_def);
sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr);
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Recent GCC builds report two warning classes in core codepaths: a
possible uninitialized read in `bound_propagator::relevant_bound`, and
repeated `-Warray-bounds` diagnostics in `mpz_manager::get_sign_cell`
when materializing small integers into a reserved `mpz_cell`.
- **Warning cleanup in bound propagation**
- Initialize `interval_size` at declaration in
`src/ast/simplifiers/bound_propagator.cpp` so the compiler can prove
safety across templated `LOWER/UPPER` instantiations using `std::clamp`.
- Preserves existing control flow and refinement heuristics (`bounded`
remains the gate for interval-based logic).
- **Warning cleanup in mpz small-value cell materialization**
- In `src/util/mpz.h`, replace direct writes through `cell->m_digits[0]`
with writes via a derived digits pointer
(`reinterpret_cast<digit_t*>(cell + 1)`), avoiding zero-length
trailing-array indexing diagnostics.
- Keeps memory layout and semantics unchanged for the stack-reserved
`sign_cell` buffer.
- **Representative change**
```cpp
cell = reserve;
cell->m_size = 1;
digit_t* cell_digits = reinterpret_cast<digit_t*>(cell + 1);
cell_digits[0] = a.value() < 0 ? -a.value() : a.value();
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This updates `src/solver/parallel_tactical2.cpp` with targeted
simplifications to align style and reduce local verbosity without
changing solver behavior. The changes are limited to member naming
consistency, cast style consistency, and a small `expr_ref` construction
cleanup.
- **`batch_manager` member naming consistency**
- Renamed the two outlier private fields to follow the existing `m_`
convention:
- `shared_clause_trail` → `m_shared_clause_trail`
- `shared_clause_set` → `m_shared_clause_set`
- Updated all corresponding reads/writes in clause collection, reset,
and clause-return paths.
- **Cast style consistency**
- Replaced C-style cast in thread count calculation with
`static_cast<unsigned>(...)` for consistency with style already used in
the file.
- **Simplified `expr_ref` construction in cube assembly**
- Collapsed default-init + assignment into direct construction when
pushing cube literals.
```cpp
// Before
expr_ref lit(g2l.to());
lit = g2l(cur->get_literal().get());
cube.push_back(std::move(lit));
// After
cube.push_back(expr_ref(g2l(cur->get_literal().get()), g2l.to()));
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Discussion #9524 reported systematic TPTP result polarity errors
(notably `Unsatisfiable/Theorem` cases returned as `Satisfiable`) and
timeout-path instability in the frontend. The dominant issue was
semantic: free variables in FOF/CNF formulas were parsed as constants
instead of implicitly universally quantified variables.
- **Parser semantics: free variables now follow TPTP rules**
- In `/home/runner/work/z3/z3/src/cmd_context/tptp_frontend.cpp`, free
variables encountered while parsing an annotated formula are now
collected in formula scope and wrapped with a top-level `forall`.
- This applies to both term and atomic-formula paths, so variable
occurrences are treated consistently.
- Explicitly bound quantifier variables continue to take precedence over
implicit ones.
- **Scoped implementation cleanup**
- Added scoped state for implicit-variable collection to avoid leaking
parser state across formulas.
- Kept variable binding order stable so quantifier construction is
deterministic.
- **Timeout-path robustness**
- Updated frontend exception catches to `const&` in the TPTP stream
entrypoint to make timeout/error handling behavior consistent with
thrown exception forms.
- **Regression tests**
- Extended `/home/runner/work/z3/z3/src/test/tptp.cpp` with focused
cases for:
- FOF free-variable implicit universal quantification.
- CNF free-variable implicit universal quantification.
```tptp
cnf(c1,axiom, p(X)).
cnf(c2,axiom, ~ p(a)).
```
This now maps to `forall X. p(X)` plus `~p(a)`, yielding `% SZS status
Unsatisfiable` as expected.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
`fpa2bv_converter::mk_to_real` computed `2^(1/|exp|)` instead of
`1/(2^|exp|)` for floats with negative exponents, causing the NRA solver
to reach contradictory conclusions and return spurious `unsat` for
satisfiable QF_FPLRA formulas.
## Root Cause
After the loop that evaluates `exp2 = |unbiased_exp|` as an integer, the
code took `1/exp2` (reciprocal of the integer) before calling
`mk_power`, yielding `2^(1/3)` instead of `2^(-3) = 1/8` for a float
with exponent -3:
```cpp
// Buggy
one_div_exp2 = mk_div(one, exp2); // 1/|exp|, not 1/2^|exp|
exp2 = mk_ite(exp_is_neg, one_div_exp2, exp2);
two_exp2 = mk_power(two, exp2); // 2^(1/3) ≠ 1/8 for exp=-3
```
## Fix
Compute the power of 2 first, then invert it:
```cpp
// Fixed
two_exp2 = mk_power(two, exp2); // 2^|exp|
one_div_two_exp2 = mk_div(one, two_exp2); // 1/(2^|exp|)
two_exp2 = mk_ite(exp_is_neg, one_div_two_exp2, two_exp2); // correct 2^exp
```
## Impact
- **QF_FPLRA**: `to_fp(RTZ, r)` with a symbolic real `r` constrained to
an interval containing a float's exact rational value now correctly
returns `sat`.
- **fp.to_real**: Fixes incorrect real-valued encoding for all floats
with negative exponents, including denormals (which adjust the exponent
by subtracting leading-zero count).
A regression test covering the reported case is added to
`src/test/fpa.cpp`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This PR targets the main TFF frontend parsing failures: bare numeric
atoms were being treated as uninterpreted terms (`U`) in formula
position, decimal literals were not parsed, and `$uminus` was not
recognized as an arithmetic builtin. These issues caused widespread
parse/type failures in arithmetic-heavy TPTP inputs.
- **Numeric atom parsing in formulas (TFF)**
- Added a shared numeric-literal parser path for term/formula contexts.
- In atomic formulas, numeric LHS now parses as arithmetic numerals
before `=`/`!=` handling, avoiding `U` vs `Int/Real` mismatches.
- **Decimal literal support**
- Extended numeral parsing to accept `d.d` forms and construct `Real`
numerals.
- Keeps existing integer (`d`) and rational (`d/d`) behavior on the same
code path.
- **`$uminus` builtin support**
- Added explicit handling for `$uminus(<arg>)` in term parsing.
- Enforces arity 1 and arithmetic-argument checks; maps directly to
arithmetic unary minus.
- **Focused regression coverage**
- Added/updated TPTP unit cases for:
- bare integer inequality: `31 != 12`
- decimal arithmetic literal usage
- `$uminus` in arithmetic predicates
Example of now-supported inputs:
```tptp
tff(c1,conjecture, 31 != 12).
tff(c2,conjecture, ~ $less(-3.25,-8.69)).
tff(c3,conjecture, $less($uminus(2),0)).
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
