Commits

Branch selector

 pure-z3

User selector

All users

All time

Commit History

Commits on Jan 30, 2026

• Improve README

  shingarov

  committed
  fcbe0c6

  Copy full SHA for fcbe0c6

Commits on Jan 4, 2026

• Fix inverted logic in HPredAnd>>pTrivial

  Show description for d108b4f
  shingarov

  committed
  d108b4f

  Copy full SHA for d108b4f

Commits on Dec 17, 2025

• [cosmetic] Typographical niceties in checkRAbs

  shingarov

  committed
  47c6c1e

  Copy full SHA for 47c6c1e

• [cosmetic] Explain relationship between our ∀ and LH-proper's

  shingarov

  committed
  456dc58

  Copy full SHA for 456dc58

Commits on Nov 24, 2025

• Add angle-bracket syntax for predicate refTops

  Show description for e6d38b2
  shingarov

  committed
  e6d38b2

  Copy full SHA for e6d38b2

• [PP] Add PPParser>>angles

  shingarov

  committed
  bdb3bd5

  Copy full SHA for bdb3bd5

Commits on Sep 24, 2025

• Sync annotation parsing with declaration parsing

  Show description for 354125d
  

  janvrany

  authored and

  shingarov

  committed
  354125d

  Copy full SHA for 354125d

Commits on Sep 21, 2025

• Don't skip L₈ test_poly now that #255 is fixed

  shingarov

  committed
  3fc23cb

  Copy full SHA for 3fc23cb

• [PLE] Implement missing cases of <=>, ==> in Z3Node>>simplifyStep:in:

  shingarov

  committed
  6e59f8a

  Copy full SHA for 6e59f8a

• Implement missing PAtom>>exprSymbolsSet

  shingarov

  committed
  77e151f

  Copy full SHA for 77e151f

Commits on Sep 17, 2025

• [Z3] Update `Float >> toBitVector:` to work also on Smalltalk/X

  Show description for 808d494
  

  janvrany

  authored and

  shingarov

  committed
  808d494

  Copy full SHA for 808d494

• [Z3] Add `Float >> toBitVector:` returning bitvector in IEEE 754 format

  

  janvrany

  authored and

  shingarov

  committed
  33e3380

  Copy full SHA for 33e3380

• [Z3] Add `Object >> toFloatingPoint:`

  Show description for 2ceef9d
  

  janvrany

  authored and

  shingarov

  committed
  2ceef9d

  Copy full SHA for 2ceef9d

• Add floating point support

  

  m-demare

  authored and

  shingarov

  committed
  fe3fe18

  Copy full SHA for fe3fe18

Commits on Sep 16, 2025

• Specify Tonel version in `src/.properties`

  Show description for 79016d4
  

  janvrany

  and

  m-demare

  committed
  79016d4

  Copy full SHA for 79016d4

Commits on Sep 15, 2025

• Show core program source after α-renaming when inspecting `Prog`

  Show description for 01b088d
  

  janvrany

  authored and

  shingarov

  committed
  01b088d

  Copy full SHA for 01b088d

• Fix printing of binary operators

  Show description for 53194fe
  

  janvrany

  authored and

  shingarov

  committed
  53194fe

  Copy full SHA for 53194fe

• Fix printing "let in let"

  Show description for 6d36956
  

  janvrany

  authored and

  shingarov

  committed
  6d36956

  Copy full SHA for 6d36956

• Add missing `SpriteRDecl >> isRecursive`

  

  janvrany

  authored and

  shingarov

  committed
  4b5ea22

  Copy full SHA for 4b5ea22

Commits on Sep 3, 2025

• Fix nasty bug in `SpriteDecl >> toANF`

  Show description for f94df82
  

  janvrany

  authored and

  shingarov

  committed
  f94df82

  Copy full SHA for f94df82

Commits on Sep 2, 2025

• Implement ECon>>isConstantNamed: before we fix #194

  shingarov

  committed
  c78ee35

  Copy full SHA for c78ee35

• Separate termination check from axiom insertion

  shingarov

  committed
  98e5ad3

  Copy full SHA for 98e5ad3

Commits on Aug 22, 2025

• [CI]: run "Z3 proper" tests also on Pharo 13

  

  janvrany

  authored and

  shingarov

  committed
  eaaee51

  Copy full SHA for eaaee51

• Fix `check-deps.st` script to work on P13

  Show description for 24b35c2
  

  janvrany

  authored and

  shingarov

  committed
  24b35c2

  Copy full SHA for 24b35c2

• [Z3] Use `#ifThen:else:` instead of `#ifTrue:ifFalse:` in some tests

  Show description for 7b3a026
  

  janvrany

  authored and

  shingarov

  committed
  7b3a026

  Copy full SHA for 7b3a026

• [Z3] Update FFI to work also in P13

  Show description for f38a13c
  

  janvrany

  authored and

  shingarov

  committed
  f38a13c

  Copy full SHA for f38a13c

Commits on Aug 21, 2025

• [Z3] Check that ASTs belong to the same context

  Show description for 3a5e6d6
  

  janvrany

  authored and

  shingarov

  committed
  3a5e6d6

  Copy full SHA for 3a5e6d6

• [Z3] Abort `apigen.py` on assertion error

  Show description for b731594
  

  janvrany

  authored and

  shingarov

  committed
  b731594

  Copy full SHA for b731594

Commits on Aug 20, 2025

• Implement Sprite "unparsing"

  Show description for 3d0dd88
  

  janvrany

  authored and

  shingarov

  committed
  3d0dd88

  Copy full SHA for 3d0dd88

Commits on Aug 18, 2025

• Update makefiles to 08e0b7e0

  

  janvrany

  authored and

  shingarov

  committed
  3817c74

  Copy full SHA for 3817c74

Commits on Aug 14, 2025

• Add a Sprite test showing how ⟦val…⟧ erases refinement

  shingarov

  committed
  6dcb6a8

  Copy full SHA for 6dcb6a8

• GT-Inspect Unsafe's counterexample

  shingarov

  committed
  d4f687b

  Copy full SHA for d4f687b

• [Z3](cosmetic) Categorize Z3Model>>gtInspectorTextIn:

  shingarov

  committed
  20517eb

  Copy full SHA for 20517eb

Commits on Jul 25, 2025

• [Z3]: Simplify `Z3CAPITest >> #testFindModel0`

  Show description for 53a2690
  

  janvrany

  authored and

  shingarov

  committed
  53a2690

  Copy full SHA for 53a2690

Commits on Jul 24, 2025

• [Z3] Fix manifest of Z3-Tests

  Show description for d5912b9
  janvrany

  committed
  d5912b9

  Copy full SHA for d5912b9

Pagination

Previous

Next