Issues

• Enum symbols are not constrained to the members of the enum

  endjin/Z3.Linq#97 · Filter by author HowardvanRooijen opened on Sep 1, 2026

• Object collections cannot be constrained or read back: a Holder[] symbol fails in every shape

  endjin/Z3.Linq#89 · Filter by author HowardvanRooijen opened on Sep 1, 2026

• A short symbol is not bounded to short's range, so Z3 can pick a value it cannot hold

  endjin/Z3.Linq#87 · Filter by author HowardvanRooijen opened on Sep 1, 2026

• No way to bound a solve: an undecidable theorem hangs the calling thread forever

  endjin/Z3.Linq#85 · Filter by author HowardvanRooijen opened on Sep 1, 2026

• DateTime symbols cannot represent anything before 1601, and fail with a bare ArgumentOutOfRangeException

  endjin/Z3.Linq#83 · Filter by author HowardvanRooijen opened on Sep 1, 2026

• XML doc comments are never validated, and the package ships none

  endjin/Z3.Linq#82 · Filter by author HowardvanRooijen opened on Sep 1, 2026
  1

• Uninitialised collection symbols throw NullReferenceException, and a ValueTuple cannot initialise one at all

  endjin/Z3.Linq#78 · Filter by author HowardvanRooijen opened on Sep 1, 2026

• float variables cannot be compared against real symbols: the widening Convert is read as int-to-real

  endjin/Z3.Linq#76 · Filter by author HowardvanRooijen opened on Sep 1, 2026

• Anonymous environment with a nested object property throws NullReferenceException

  endjin/Z3.Linq#75 · Filter by author HowardvanRooijen opened on Sep 1, 2026

• Only int collections work: every other element type fails with a Z3 sort error

  endjin/Z3.Linq#64 · Filter by author HowardvanRooijen opened on Sep 1, 2026
  3

• short symbols are unusable: every theorem over a short throws

  endjin/Z3.Linq#63 · Filter by author HowardvanRooijen opened on Sep 1, 2026
  1

• Hold Z3.Linq releases until Microsoft.Z3 is published to nuget.org

  endjin/Z3.Linq#60 · Filter by author HowardvanRooijen opened on Sep 1, 2026

• Optimize returns null through a non-nullable T when unsatisfiable

  endjin/Z3.Linq#58 · Filter by author HowardvanRooijen opened on Sep 1, 2026
  1

• Unsatisfiable theorems over value types are indistinguishable from a valid all-zero solution

  endjin/Z3.Linq#57 · Filter by author HowardvanRooijen opened on Sep 1, 2026
  1

• DateTime round-trip shifts by the UTC offset outside GMT

  endjin/Z3.Linq#56 · Filter by author HowardvanRooijen opened on Sep 1, 2026

• decimal[] elements all get the same value: element loop evaluates the whole array expression

  endjin/Z3.Linq#55 · Filter by author HowardvanRooijen opened on Sep 1, 2026
  1

• float symbols cannot round-trip: TypeCode.Single reads back as double

  endjin/Z3.Linq#54 · Filter by author HowardvanRooijen opened on Sep 1, 2026

• Collection-typed public fields throw: FieldInfo is cast to ICollection instead of its value

  endjin/Z3.Linq#53 · Filter by author HowardvanRooijen opened on Sep 1, 2026

• MkReal is culture-sensitive: real constants break under comma-decimal cultures

  endjin/Z3.Linq#52 · Filter by author HowardvanRooijen opened on Sep 1, 2026
  1

• Solve() throws InvalidCastException when a symbol is unconstrained

  endjin/Z3.Linq#51 · Filter by author HowardvanRooijen opened on Sep 1, 2026

• How to get all solutions from a theorem?

  endjin/Z3.Linq#41 · Filter by author LittleLittleCloud opened on Oct 22, 2024
  1

• Cannot use expressions in place of variables

  endjin/Z3.Linq#36 · Filter by author VelizarHristov opened on Dec 27, 2023

• Other improvements available

  endjin/Z3.Linq#29 · Filter by author jsboige opened on Aug 30, 2023
  13

• Checking for unsatisfiability when using ValueTuple

  endjin/Z3.Linq#28 · Filter by author NickRedwood opened on Aug 2, 2023
  3

• Approach advice requested

  endjin/Z3.Linq#10 · Filter by author WhitWaldo opened on Sep 28, 2022
  4