Skip to content

Improve generation accounting (#10008)#10009

Open
NikolajBjorner wants to merge 5 commits into
masterfrom
generation
Open

Improve generation accounting (#10008)#10009
NikolajBjorner wants to merge 5 commits into
masterfrom
generation

Conversation

@NikolajBjorner

@NikolajBjorner NikolajBjorner commented Jun 30, 2026

Copy link
Copy Markdown
Contributor

Details in original PR: #10007

@CanCebeci
Improve generation accounting (#10008)
03572a6 
Details in original PR: #10007

---------

Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
@CanCebeci

CanCebeci commented Jun 30, 2026

Copy link
Copy Markdown
Collaborator

Updated Mariposa results:

Performance

Timeline on Mariposa's unsat core:

Version #Queries with unknowns (/58) Total # unknowns 60sec timeouts (/5699)
Before May 7th 28 522 1818
May 7th - 'Use the minimum generation number among matching enodes' 22 355 1978
May 26th - 'Update generation number of already-internalized enodes' 16 117 2040
June 4 - 'Cleaner fix for initializing and finalizing m_max...' (only on CanCebeci/z3) 7 56 2399
June 29th (original PR) - 'Debug undo_add_eq, treat eqs as gen0' 7 62 1924
June 30th (current) - 'Remember to account for equalities..' 5 58 1867

@CanCebeci

CanCebeci commented Jul 1, 2026

Copy link
Copy Markdown
Collaborator

Results over quantified SMTLIB benchmarks:

Biggest regressions, sorted by solved delta:

  • ALIA: -14/1262
  • ABV: -8/1756
  • AUFBVDTNIRA: -4/3413
  • UF: -4/2737
  • UFDTLIRA: -4/7042

Biggest improvements, sorted by solved delta:

  • UFLIA: +7/7173
  • UFFPDTNIRA: +1/618
  • UFDTNIRA: +1/3983
  • UFBVLIA: +1/1
  • UFBVFPDTNIRA: +1/44
Category total solved sat unsat unknown timeout baseline total solved baseline sat baseline unsat baseline unknown baseline timeout Delta solved/baseline solved
ABV 1748 1436 312 2736 491 1756 1445 311 2739 480 -8/1756
ABVFP 32 30 2 19 9 32 30 2 19 9 +0/32
ABVFPLRA 63 59 4 14 0 63 59 4 14 0 +0/63
ALIA 1248 958 290 1616 234 1262 969 293 1603 233 -14/1262
ANIA 42 31 11 22 14 42 31 11 22 14 +0/42
AUFBV 379 131 248 10 1134 380 131 249 10 1133 -1/380
AUFBVDTLIA 484 109 375 9 1190 487 109 378 10 1186 -3/487
AUFBVDTNIA 509 1 508 0 43 509 1 508 0 43 +0/509
AUFBVDTNIRA 3409 0 3409 0 1632 3413 0 3413 0 1628 -4/3413
AUFBVFP 9 3 6 0 48 9 3 6 0 48 +0/9
AUFBVFPDTNIRA 53 0 53 0 64 53 0 53 0 64 +0/53
AUFDTLIA 742 46 696 0 53 743 46 697 0 52 -1/743
AUFDTLIRA 9889 0 9889 139 1015 9889 0 9889 139 1015 +0/9889
AUFDTNIRA 1266 0 1266 6 295 1266 0 1266 6 295 +0/1266
AUFFPDTNIRA 139 0 139 8 19 139 0 139 8 19 +0/139
AUFLIA 2570 339 2231 35 722 2571 340 2231 35 721 -1/2571
AUFLIRA 19598 63 19535 0 413 19597 64 19533 0 414 +1/19597
AUFNIA 0 0 0 0 3 0 0 0 0 3 +0/0
AUFNIRA 1024 5 1019 2 454 1024 5 1019 2 454 +0/1024
BV 5580 563 5017 0 605 5580 563 5017 0 605 +0/5580
BVFP 172 161 11 4 32 172 161 11 4 32 +0/172
BVFPLRA 211 199 12 1 54 212 200 12 1 53 -1/212
FP 1765 6 1759 10 894 1764 6 1758 10 895 +1/1764
FPLRA 24 24 0 0 17 n/a n/a n/a n/a n/a +24/n/a
LIA 424 162 262 0 112 n/a n/a n/a n/a n/a +424/n/a
LRA 2077 744 1333 0 362 2077 744 1333 0 362 +0/2077
NIA 214 73 141 0 43 214 73 141 0 43 +0/214
NRA 3813 3 3810 0 6 3813 3 3810 0 6 +0/3813
UF 2733 109 2624 0 4857 2737 109 2628 0 4853 -4/2737
UFBV 138 37 101 0 55 138 37 101 0 55 +0/138
UFBVDT 0 0 0 0 1 0 0 0 0 1 +0/0
UFBVDTLIA 24 0 24 0 0 24 0 24 0 0 +0/24
UFBVDTNIA 157 0 157 0 0 157 0 157 0 0 +0/157
UFBVDTNIRA 993 0 993 0 266 994 0 994 0 265 -1/994
UFBVFP 1 0 1 0 1 1 0 1 0 1 +0/1
UFBVFPDTNIRA 45 0 45 0 44 44 0 44 0 45 +1/44
UFBVLIA 2 0 2 0 206 1 0 1 0 207 +1/1
UFDT 1844 21 1823 7 2718 1845 20 1825 8 2716 -1/1845
UFDTLIA 1270 0 1270 0 313 1272 0 1272 0 311 -2/1272
UFDTLIRA 7038 1209 5829 1 710 7042 1212 5830 1 706 -4/7042
UFDTNIA 976 0 976 0 32 978 0 978 0 30 -2/978
UFDTNIRA 3984 38 3946 0 440 3983 38 3945 0 441 +1/3983
UFFPDTNIRA 619 60 559 0 176 618 59 559 0 177 +1/618
UFIDL 57 2 55 0 11 57 2 55 0 11 +0/57
UFLIA 7180 15 7165 1 2947 7173 15 7158 1 2954 +7/7173
UFLRA 12 2 10 0 3 12 2 10 0 3 +0/12
UFNIRA 109 15 94 6 151 110 15 95 6 150 -1/110

@NikolajBjorner
fix signature regression for unit test
e7e6861 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner

NikolajBjorner commented Jul 2, 2026

Copy link
Copy Markdown
Contributor Author

┌───────────────┬────────────────┬──────────────┬───────┬────────────────┬──────────────┬─────────┐
│ Benchmark │ Solved (https) │ Solved (gen) │ Delta │ Time https (s) │ Time gen (s) │ Speedup │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_ABV │ 14681 │ 14678 │ −3 │ 13456.9 │ 13517.7 │ 0.995 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_ABVFP │ 17513 │ 17509 │ −4 │ 21667.3 │ 21808.9 │ 0.994 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_ABVFPLRA │ 56 │ 57 │ +1 │ 385.8 │ 383.5 │ 1.006 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_ALIA │ 124 │ 123 │ −1 │ 1237.1 │ 1255.1 │ 0.986 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_ANIA │ 74 │ 73 │ −1 │ 1856.2 │ 1865.0 │ 0.995 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_AUFBV │ 43 │ 43 │ 0 │ 668.2 │ 670.2 │ 0.997 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_AUFBVFP │ 0 │ 0 │ 0 │ 20.0 │ 20.0 │ 1.000 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_AUFLIA │ 1303 │ 1303 │ 0 │ 105.8 │ 115.8 │ 0.913 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_AUFNIA │ 17 │ 17 │ 0 │ 18.3 │ 19.9 │ 0.917 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_AX │ 551 │ 551 │ 0 │ 54.4 │ 46.1 │ 1.182 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_BV │ 39804 │ 39804 │ 0 │ 174551.0 │ 174551.8 │ 1.000 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_BVFP │ 17127 │ 17127 │ 0 │ 7246.6 │ 7286.3 │ 0.995 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_BVFPLRA │ 109 │ 109 │ 0 │ 1930.6 │ 1935.8 │ 0.997 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_DT │ 8163 │ 8160 │ −3 │ 11923.5 │ 11992.3 │ 0.994 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_FP │ 40189 │ 40189 │ 0 │ 13893.1 │ 14632.1 │ 0.949 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_FPLRA │ 33 │ 33 │ 0 │ 783.7 │ 784.1 │ 0.999 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_IDL │ 1604 │ 1610 │ +6 │ 22626.0 │ 22610.6 │ 1.001 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_LIA │ 11253 │ 11244 │ −9 │ 55125.0 │ 55395.3 │ 0.995 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_LIRA │ 5 │ 5 │ 0 │ 43.1 │ 43.2 │ 0.997 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_LRA │ 1254 │ 1251 │ −3 │ 11935.6 │ 11952.2 │ 0.999 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_NIA │ 17099 │ 17064 │ −35 │ 220730.6 │ 220842.6 │ 0.999 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_NIRA │ 2 │ 2 │ 0 │ 23.3 │ 23.3 │ 0.998 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_NRA │ 10592 │ 10592 │ 0 │ 36796.6 │ 36839.1 │ 0.999 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_RDL │ 189 │ 188 │ −1 │ 1780.5 │ 1782.9 │ 0.999 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_S │ 18377 │ 18375 │ −2 │ 64801.0 │ 64856.9 │ 0.999 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_SLIA │ 75760 │ 75740 │ −20 │ 226751.7 │ 228165.9 │ 0.994 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_SNIA │ 70 │ 70 │ 0 │ 2.8 │ 2.6 │ 1.043 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_UF │ 7488 │ 7488 │ 0 │ 1946.4 │ 2045.3 │ 0.952 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_UFBV │ 1508 │ 1495 │ −13 │ 24871.0 │ 24937.8 │ 0.997 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_UFBVDT │ 10 │ 10 │ 0 │ 1409.2 │ 1410.1 │ 0.999 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_UFDT │ 4 │ 3 │ −1 │ 4012.0 │ 4011.5 │ 1.000 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_UFDTLIA │ 47 │ 47 │ 0 │ 748.6 │ 748.4 │ 1.000 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_UFDTLIRA │ 146 │ 146 │ 0 │ 9.9 │ 8.0 │ 1.230 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_UFDTNIA │ 44 │ 44 │ 0 │ 905.4 │ 913.0 │ 0.992 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_UFFP │ 2 │ 2 │ 0 │ 12.2 │ 12.5 │ 0.974 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_UFFPDTNIRA │ 148 │ 148 │ 0 │ 199.7 │ 198.9 │ 1.004 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_UFIDL │ 501 │ 501 │ 0 │ 3251.3 │ 3314.8 │ 0.981 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_UFLIA │ 612 │ 611 │ −1 │ 1212.5 │ 1212.4 │ 1.000 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_UFLRA │ 1251 │ 1251 │ 0 │ 1033.1 │ 1040.6 │ 0.993 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ QF_UFNRA │ 55 │ 55 │ 0 │ 158.4 │ 158.9 │ 0.997 │
├───────────────┼────────────────┼──────────────┼───────┼────────────────┼──────────────┼─────────┤
│ TOTAL │ 287808 │ 287718 │ −90 │ 930184 │ 933412 │ 0.997 │
└───────────────┴────────────────┴──────────────┴───────┴────────────────┴──────────────┴─────────┘

@NikolajBjorner

NikolajBjorner commented Jul 2, 2026

Copy link
Copy Markdown
Contributor Author
  • check QF_UF if the 5% time regression is real.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@NikolajBjorner @CanCebeci