Commit graph

mirrors/z3

Fork 0

mirror of https://github.com/Z3Prover/z3 synced 2026-08-10 07:51:20 +00:00

Select branches

Hide pull requests

arie

arith-round-robin

c3-budget

c3-merge-master

c3-replace-term

c3-split-marker

c3-split-perf

c3_power_vs_power_case

code-simplifier/fix-optional-type-hints-a468a3c36adfd68c

code-simplifier/fix-pop-app-frame-indentation-d94e72b433144153

code-simplifier/mbp-array-index-cleanup-9f49472022a01c7c

code-simplifier/model-core-cleanup-53966070efa0376a

code-simplifier/nra-solver-clarity-a0fd52ea3e629ee8

code-simplifier/parallel-cmake-build-5e927099830f755a

code-simplifier/remove-redundant-phase-assignment-aa4bd56e7fb7e814

code-simplifier/remove-unused-defined-names-fed46dd0fdcfc07b

code-simplifier/seq-monadic-cleanup-4bcf9b16358a0f98

copilot/add-parikh-filter-implementation

copilot/add-tests-requested-by-wintersteiger

copilot/align-coding-conventions-z3

copilot/alternative-z3-solver-solutions

copilot/apply-suggested-fixes-to-tests

copilot/change-release-notes-action

copilot/check-artifact-retention

copilot/check-porting-options-seq-nielsen

copilot/create-workflow-for-z3-and-zipt

copilot/davedets-master-to-detlefs

copilot/diagnose-failures

copilot/diagnose-query-failures

copilot/feature-monomial-bounds-analysis

copilot/fix-assertion-violation

copilot/fix-assertion-violation-vector-h

copilot/fix-build-errors-z3-test

copilot/fix-build-issue

copilot/fix-build-warning-fixer-workflow

copilot/fix-failing-build-and-report-job

copilot/fix-fpa-soundness-issue

copilot/fix-inaccurate-optimal-value

copilot/fix-invalid-model-generation

copilot/fix-invalid-model-proof-generation

copilot/fix-mcp-server-output-issues

copilot/fix-missing-override-keyword

copilot/fix-missing-test-files

copilot/fix-objective-value-reporting

copilot/fix-overflow-vector-error

copilot/fix-segfault-regression-trunk

copilot/fix-segmentation-fault

copilot/fix-segmentation-fault-again

copilot/fix-segmentation-fault-another-one

copilot/fix-segmentation-fault-one-more-time

copilot/fix-segmentation-fault-yet-again

copilot/fix-sigsegv-in-mbqi-model-checker

copilot/fix-sigsegv-non-linear-query

copilot/fix-smtlib-crash

copilot/fix-solution-soundness-bug

copilot/fix-string-solver-performance-regression

copilot/fix-tagged-pointer-bug

copilot/fix-undeclared-identifier-p

copilot/fix-warning-extra-semi

copilot/fix-warning-messages

copilot/fix-warnings-in-code

copilot/fix-workflows

copilot/fix-z3-crash-fstar-example

copilot/fix-z3py-spacer-crash

copilot/historical-nlsat-regression-tests

copilot/issn000-fix-issue

copilot/refactor-factor-rewriter-structured-bindings

copilot/refactor-theory-bv-structured-bindings

copilot/revert-range-based-loops

copilot/run-deep-test-on-z3

copilot/swap-order-names

copilot/update-code-conventions-analyzer

copilot/update-code-review-remarks

copilot/update-euf-snode-support

copilot/update-seq-nielsen-handle-equations

copilot/zipt-review-sls-seq-plugin-code-improvements

copilot/zipt-review-sls-seq-plugin-code-quality-improvemen

copilot/zipt-review-string-graph-improvements

efficacy-cut-filter

faster_find_fs

fix-10385-cg-generation

fix-10417

fix-build-warnings

fix-div0-define-fun-collision-ca8c66d66fad09b9

fix-regex-range-collapse-test-portability

fix/clang-tidy-dead-stores-d3bc9f4cec0022d3

fix/div0-model-reparse-iss3172-3bc9076621ca90fe

fix/nl-propagate-fixed-rows-regression-10304-4909e97621096167

fmcad26_artifact

fstar-build-fix/priorityqueue-4-nla-fixed-rows-aa4023f3df510d48

fstar-fix-priorityqueue-nl-propagate-fixed-rows-0185235f45af0a37

fstar-opt-improved

fstar-opt-symbolic

gomory-cut-history

gomory-ortho-master

iss8185

linprobe

lll_cube

lprobe

master

nla-aeq

optimize-nl-bounds

poly

polysat

pyodide-ci

refine-terms

seq-dnf-opt

seq-length-lookahead

seq-monadic-budget

seq-monadic-sl

seq-monidic-core

seq-split

simplify/choice-axiom-consistency-e33de7949014eecb

smtmus

split_set

synth

veanes-derive

veanes/range-set-integration

xor

#1000

#10001

#10002

#10003

#10006

#10007

#10008

#10009

#10014

#10015

#10016

#10017

#1002

#10020

#10021

#10022

#10023

#10024

#10029

#10030

#10031

#10032

#10034

#10035

#10038

#10039

#1004

#10040

#10041

#10042

#10047

#10048

#10049

#10050

#10051

#10052

#10054

#10057

#10059

#10062

#10063

#10064

#10066

#10067

#10068

#1007

#10071

#10073

#10075

#10076

#10077

#10078

#10080

#10081

#10082

#10084

#10085

#10086

#10087

#10088

#10089

#10090

#10091

#10093

#10094

#10095

#10096

#10097

#10098

#10099

#1010

#10100

#10101

#10102

#10103

#10104

#10105

#10106

#10107

#10109

#10110

#10111

#10112

#10115

#10116

#10118

#10119

#10120

#10121

#10122

#10126

#10127

#10129

#1013

#10132

#10135

#10138

#10139

#10140

#10141

#10142

#10143

#10144

#10146

#10147

#10148

#10149

#10150

#10151

#10154

#10155

#10156

#10157

#10158

#10163

#10165

#10169

#1017

#10174

#10179

#1018

#10180

#10181

#10182

#10183

#10184

#10185

#10186

#10188

#10189

#10190

#10191

#10192

#10193

#10194

#10195

#10199

#1020

#10200

#10201

#10202

#10203

#10204

#10208

#10209

#10210

#10211

#10212

#10216

#10217

#10219

#10221

#10222

#10223

#10224

#10227

#10228

#10229

#10230

#10231

#10237

#10238

#1024

#10242

#10243

#10244

#10245

#10246

#10249

#10253

#10254

#10255

#10256

#1026

#10261

#10262

#10263

#10266

#10269

#10277

#10279

#10284

#10286

#10289

#10290

#10292

#10294

#10295

#10296

#10298

#10300

#10301

#10302

#10304

#10305

#10307

#10309

#1031

#10310

#10311

#10312

#10313

#10314

#10315

#10317

#10318

#10319

#10320

#10323

#10325

#10326

#10327

#10329

#1033

#10330

#10332

#10334

#10336

#10341

#10342

#10343

#10344

#10345

#10346

#10347

#10348

#10349

#10350

#10351

#10354

#10355

#1036

#10360

#10361

#10362

#10364

#10365

#10366

#10369

#1037

#10370

#10371

#10373

#10376

#10381

#10383

#10384

#10386

#10389

#10390

#10391

#10392

#10393

#10397

#10398

#10399

#104

#1040

#10401

#10402

#10407

#10408

#10411

#10412

#10414

#10415

#10418

#10419

#10421

#10423

#10424

#10428

#10429

#10431

#10433

#10434

#10438

#10439

#10440

#10442

#10444

#10445

#10446

#10447

#10448

#10449

#10451

#10452

#10453

#10454

#10455

#10456

#10458

#10459

#10460

#10466

#10467

#10468

#10470

#1049

#1050

#106

#1066

#1069

#107

#1070

#1073

#1076

#108

#1084

#1089

#1090

#1091

#1094

#1095

#1096

#1099

#11

#1104

#1105

#1110

#1111

#1114

#1115

#1117

#1119

#1126

#1129

#1131

#1136

#1138

#1142

#1144

#1145

#1146

#1147

#1158

#1162

#1166

#117

#1174

#1181

#1182

#1183

#1185

#1188

#1189

#12

#1205

#1207

#1208

#1216

#1220

#1222

#1225

#1226

#1228

#1229

#1232

#1238

#1253

#1256

#1259

#126

#1262

#127

#1270

#1271

#128

#1280

#1281

#1282

#1289

#130

#1300

#1301

#1307

#1312

#1315

#1323

#1324

#1325

#1336

#1337

#1338

#134

#1341

#1351

#1355

#1360

#1363

#1381

#1385

#1391

#1396

#1400

#1401

#1410

#1412

#1430

#1431

#1432

#1433

#1434

#1435

#1436

#1438

#1440

#1453

#146

#1462

#1464

#1465

#1466

#1467

#147

#1472

#1473

#1474

#1478

#1479

#1480

#1482

#1483

#1485

#1486

#1487

#1494

#1495

#1497

#15

#1501

#1503

#1506

#1508

#1517

#1518

#1519

#152

#1527

#1528

#1537

#1541

#1542

#1546

#155

#1552

#1556

#1557

#1559

#1560

#1562

#1565

#1588

#1591

#1596

#1597

#16

#1606

#1610

#1611

#1612

#1613

#1624

#1630

#1631

#1635

#164

#1640

#1641

#1642

#1646

#1650

#1651

#1656

#166

#1660

#1666

#1669

#1671

#1673

#1679

#1684

#1686

#1687

#169

#1691

#1692

#1693

#1697

#170

#1700

#1701

#1705

#1706

#1707

#1708

#1709

#1710

#1715

#1716

#172

#1721

#1723

#1724

#1727

#1728

#173

#1731

#1732

#1737

#1738

#1740

#1743

#1744

#1747

#1748

#1750

#1751

#1756

#1758

#1771

#1773

#1774

#1775

#1777

#1779

#1781

#1790

#1792

#1796

#1797

#1799

#18

#1809

#1815

#1818

#1823

#1826

#1829

#1834

#1837

#1838

#1839

#1840

#1843

#1845

#1848

#1849

#1850

#1852

#1853

#1854

#1855

#1856

#1857

#1858

#1859

#1860

#1861

#1862

#1863

#1865

#1867

#1869

#1873

#1876

#1877

#1878

#188

#1880

#1881

#1883

#1884

#1886

#1887

#1888

#1893

#1894

#1902

#1906

#1915

#1918

#1930

#1931

#1935

#1938

#1939

#1942

#1947

#1949

#1950

#1951

#1952

#1954

#1955

#1960

#1963

#1964

#1967

#1969

#1972

#1973

#1974

#1975

#1976

#1977

#1982

#1983

#1986

#1990

#1991

#1992

#1993

#1995

#1996

#1997

#1998

#1999

#2001

#2002

#2003

#2004

#2005

#2008

#2010

#2011

#2012

#2013

#2014

#2015

#2016

#2017

#2020

#2021

#2024

#2025

#2026

#2032

#2033

#2034

#2049

#2050

#2051

#2052

#2056

#2062

#2064

#2065

#2066

#2073

#2084

#2088

#21

#2103

#2105

#2121

#2124

#2132

#2133

#2143

#2146

#2147

#2148

#2150

#2163

#2166

#2167

#2170

#218

#2180

#2181

#2183

#2189

#2192

#2193

#2204

#2206

#2224

#2227

#2229

#2233

#2264

#2275

#2280

#2281

#2283

#2292

#2294

#23

#2311

#2312

#2313

#2315

#2329

#2330

#2334

#2335

#2338

#2339

#234

#2345

#235

#2356

#236

#2368

#238

#2382

#2383

#2389

#2393

#2399

#24

#242

#2428

#2438

#244

#2454

#2455

#2459

#246

#2462

#2463

#2464

#2465

#2472

#2475

#2477

#2482

#2485

#2486

#2488

#2490

#2492

#2493

#2494

#2495

#2496

#2499

#2528

#2529

#253

#2538

#2540

#2541

#2545

#255

#2550

#2554

#256

#2568

#2594

#26

#2600

#261

#2611

#2614

#2620

#2627

#2628

#2634

#2635

#2638

#2639

#2645

#2648

#2651

#2655

#2660

#2661

#267

#2677

#268

#2683

#270

#271

#2710

#2719

#272

#273

#2730

#2731

#2732

#2738

#2739

#274

#2745

#2746

#275

#2754

#276

#2769

#2786

#280

#282

#283

#2834

#2839

#284

#2846

#285

#2853

#2858

#286

#2862

#2864

#287

#2876

#2880

#2881

#289

#2893

#2895

#2899

#2907

#2931

#2940

#2942

#2947

#295

#296

#2964

#2971

#2972

#298

#2987

#2988

#299

#2997

#2999

#3002

#3007

#3008

#303

#3032

#3048

#305

#3050

#3059

#306

#309

#3091

#3093

#3094

#3095

#3097

#310

#3102

#3112

#3117

#3139

#321

#3228

#329

#33

#3321

#334

#3368

#338

#3394

#340

#344

#3445

#346

#347

#349

#3498

#350

#351

#3541

#355

#356

#357

#3596

#3617

#362

#363

#3671

#3687

#37

#3706

#373

#374

#3745

#375

#378

#379

#380

#3818

#3821

#3823

#385

#3851

#3875

#389

#390

#3900

#394

#3946

#3950

#396

#3965

#398

#401

#4011

#4043

#4056

#4059

#4068

#4070

#4072

#4075

#408

#409

#4092

#4094

#4101

#412

#413

#414

#4157

#4160

#4170

#4184

#4198

#4199

#4205

#4206

#4207

#4215

#4247

#4248

#4249

#4253

#4254

#427

#4274

#4276

#4277

#4278

#4298

#4312

#4313

#4319

#4320

#4321

#4325

#4329

#4331

#4333

#4341

#4342

#4356

#4358

#4360

#4361

#4368

#437

#4381

#4382

#4384

#4385

#4386

#4397

#4399

#441

#4413

#4415

#4420

#444

#4440

#4443

#446

#4462

#4464

#4468

#4472

#4477

#4482

#4484

#4487

#4488

#449

#4490

#4492

#4495

#4496

#4499

#4501

#4504

#4505

#4506

#4509

#4514

#4516

#4517

#4528

#4529

#453

#4535

#4545

#4550

#4551

#4556

#4558

#4560

#4562

#4585

#459

#4595

#4596

#4597

#4598

#4599

#4602

#4603

#4605

#461

#4610

#4611

#4612

#4617

#4619

#4620

#4621

#4629

#4636

#4638

#4647

#4650

#4654

#4656

#4657

#4658

#4659

#466

#4663

#4666

#4667

#467

#4674

#4676

#468

#4681

#4682

#4684

#4685

#4692

#4693

#4695

#4698

#470

#4703

#4705

#4707

#4709

#471

#4710

#4714

#4719

#4722

#4723

#4729

#4733

#4739

#4741

#4748

#4751

#4753

#4755

#4757

#4759

#4760

#4761

#4771

#4782

#4785

#4803

#4818

#483

#4832

#4833

#484

#4846

#4850

#4857

#486

#4864

#487

#4878

#4887

#49

#490

#4906

#4911

#4915

#4917

#4954

#4958

#4959

#4960

#4976

#498

#4981

#499

#4996

#500

#5001

#5003

#5004

#5005

#5008

#5015

#5021

#503

#5038

#5039

#504

#5040

#505

#5055

#506

#5079

#5081

#5082

#5091

#5097

#5098

#5104

#5105

#5116

#5118

#5120

#5128

#513

#5130

#5155

#5156

#516

#5163

#5165

#5169

#517

#5170

#5171

#5172

#5173

#5174

#5175

#5176

#5177

#5180

#5182

#5183

#5184

#5185

#5186

#5187

#5188

#5189

#519

#5190

#5191

#5192

#5194

#5195

#5198

#5199

#5200

#5201

#5202

#5203

#5209

#521

#5214

#5217

#5218

#5220

#5221

#5222

#5227

#5228

#523

#5230

#5231

#5234

#5240

#5241

#5242

#5246

#525

#5251

#526

#5265

#5268

#527

#5275

#528

#5288

#529

#5290

#5291

#5292

#5293

#5295

#531

#5310

#5311

#5322

#5326

#5327

#5332

#5348

#5351

#5353

#5355

#5360

#5364

#5366

#5368

#5369

#537

#5370

#5371

#5372

#5383

#5385

#5386

#5387

#5389

#539

#540

#5411

#5413

#5416

#5431

#5440

#5442

#5444

#545

#5451

#5453

#5458

#5459

#5463

#5466

#5475

#5477

#5483

#5489

#5496

#55

#550

#5512

#5513

#5514

#552

#5520

#5521

#5524

#5525

#5529

#553

#5534

#5536

#554

#5540

#5547

#5549

#5550

#5555

#5567

#5569

#5585

#5587

#5588

#5600

#5601

#5602

#5607

#5616

#5617

#5618

#5620

#5622

#5625

#5626

#5628

#5631

#5632

#5633

#5634

#5640

#5654

#566

#5669

#568

#5690

#5695

#5696

#5697

#5703

#5709

#5717

#5721

#5723

#5724

#5728

#5729

#5730

#5731

#5739

#575

#5756

#576

#5760

#5762

#5782

#5787

#580

#5821

#583

#5832

#5835

#5839

#5843

#5844

#5845

#5854

#5859

#5864

#5868

#5878

#5879

#5881

#5884

#5888

#5892

#5893

#5897

#5898

#5901

#5902

#5905

#5916

#5921

#5923

#5944

#5947

#5951

#5956

#5960

#5963

#5964

#5966

#597

#5971

#5972

#5974

#5975

#5976

#5977

#5978

#5979

#598

#5982

#5992

#5994

#5996

#5997

#600

#6000

#6003

#601

#6010

#6025

#6026

#6029

#603

#6035

#6037

#6048

#606

#6063

#6064

#6065

#6066

#6067

#6068

#6069

#6072

#6073

#6074

#6075

#6077

#608

#6086

#6093

#6096

#6099

#6101

#6102

#6103

#6118

#6120

#6125

#6136

#6139

#6146

#6148

#6150

#6152

#6156

#6161

#6162

#6166

#6175

#618

#6185

#6186

#6188

#6189

#6191

#6192

#6195

#6198

#6199

#6202

#6203

#6204

#6207

#6209

#621

#6210

#6211

#6216

#6217

#6219

#622

#6220

#6221

#6222

#6223

#6224

#6225

#6226

#6227

#6231

#6232

#6233

#6234

#6235

#6236

#6238

#6239

#6242

#6245

#6246

#6247

#6249

#6251

#6252

#6253

#6254

#6256

#6257

#6261

#6266

#6269

#627

#6277

#6278

#6280

#6284

#6287

#6290

#6291

#6297

#630

#6306

#6307

#6312

#6318

#6321

#6325

#6327

#6329

#6332

#6345

#6353

#6358

#6360

#6361

#6362

#6378

#6381

#639

#6393

#6402

#6405

#6406

#641

#6411

#6412

#6419

#6420

#6422

#6424

#6434

#6435

#6448

#6449

#645

#6458

#646

#6468

#6472

#648

#6483

#6489

#6497

#6509

#6514

#6516

#6526

#6527

#6528

#6529

#6533

#6534

#6540

#6541

#6549

#6562

#6567

#6569

#6576

#6596

#6597

#6608

#661

#6612

#6613

#6618

#6619

#6623

#6625

#6626

#6627

#6628

#6639

#6653

#6656

#6663

#6673

#6678

#6707

#6712

#6715

#6720

#6723

#6733

#6739

#675

#6750

#6755

#6756

#6759

#6765

#6771

#6772

#6773

#6774

#6779

#6780

#6786

#6791

#6795

#6797

#6803

#6814

#6816

#6820

#6829

#6831

#6833

#6834

#6840

#6841

#6844

#6845

#6846

#6859

#6862

#6863

#6864

#6867

#6875

#6878

#6879

#6883

#6884

#6887

#6888

#6895

#6896

#6905

#6906

#6909

#6910

#6911

#6929

#6931

#6932

#6938

#6939

#6940

#6948

#6949

#695

#6954

#6960

#6961

#6963

#6966

#6968

#6973

#6975

#6976

#6979

#6980

#6985

#6992

#6993

#6999

#700

#7002

#7008

#7013

#7014

#7015

#7016

#7019

#7021

#7022

#7025

#7028

#7030

#7034

#7039

#7042

#7043

#7044

#7045

#7051

#7052

#7054

#7057

#7058

#7059

#7060

#7063

#7065

#7066

#7067

#7068

#7069

#7071

#7075

#7077

#708

#7088

#7095

#7097

#7099

#710

#7108

#7115

#7116

#7118

#7119

#713

#7131

#7133

#7136

#7137

#7138

#7139

#7140

#7145

#7147

#7148

#7149

#715

#7150

#7152

#7153

#7155

#7157

#7159

#7163

#7169

#7170

#7171

#7173

#7184

#7192

#7200

#722

#7226

#7227

#7230

#7235

#7244

#7251

#7254

#7257

#7261

#7265

#7269

#7271

#728

#7280

#7288

#7289

#729

#7293

#7294

#7296

#7297

#7298

#7299

#73

#730

#7300

#7301

#7303

#7304

#7307

#7308

#7312

#7313

#7316

#7317

#7320

#7322

#7323

#7324

#7327

#7328

#7333

#7337

#7338

#7339

#735

#7350

#7351

#7353

#7354

#7356

#736

#7365

#737

#7384

#7387

#7388

#739

#7396

#74

#7400

#7401

#7408

#741

#7412

#742

#7422

#7423

#7426

#7428

#7429

#7437

#7439

#7442

#7452

#746

#7462

#7469

#747

#7471

#7473

#7477

#7479

#7480

#7481

#7495

#7496

#7497

#7498

#75

#750

#7503

#7504

#7506

#7508

#7514

#7516

#7519

#752

#7529

#7530

#7531

#7533

#7534

#7535

#7537

#7540

#7545

#7547

#7548

#7551

#7553

#7557

#7565

#757

#7576

#7577

#7579

#7587

#759

#7597

#7598

#7599

#76

#760

#7608

#761

#7610

#7612

#7613

#7614

#7615

#7617

#7618

#7619

#7620

#7628

#7631

#764

#7645

#7646

#7649

#7651

#7652

#7653

#7654

#7656

#7657

#7660

#7662

#7666

#7672

#7681

#7686

#7688

#7689

#7691

#7693

#7695

#7696

#7698

#7701

#7703

#7704

#7705

#7706

#7708

#7710

#7711

#7712

#7713

#7714

#7716

#7717

#7719

#7721

#7726

#7729

#7734

#7737

#7741

#7748

#7751

#7752

#7755

#7756

#7758

#7759

#7761

#7764

#7766

#7768

#7769

#7771

#7773

#7774

#7775

#7777

#7778

#7780

#7782

#7783

#7785

#7787

#7788

#779

#7790

#7793

#7794

#7795

#780

#7802

#7803

#7804

#7807

#7808

#7809

#7810

#7811

#7812

#7813

#7814

#7815

#7819

#7820

#7821

#7823

#7824

#7827

#7829

#7830

#7831

#7832

#7833

#7834

#7835

#7836

#7838

#7839

#7840

#7844

#7845

#7846

#7847

#7848

#7849

#7851

#7852

#7854

#7856

#7858

#7860

#7862

#7863

#7865

#7866

#7868

#7870

#7871

#7877

#7878

#7879

#7880

#7881

#7882

#7885

#7886

#7887

#7888

#7889

#789

#7890

#7892

#7894

#7896

#7898

#7899

#79

#7900

#7901

#7902

#7904

#7905

#7906

#7907

#7908

#7909

#7910

#7911

#7912

#7914

#7915

#7916

#7917

#7918

#7919

#7920

#7921

#7922

#7923

#7924

#7925

#7926

#7927

#7928

#7929

#7930

#7931

#7932

#7935

#7938

#7939

#7942

#7945

#7947

#7954

#7955

#7959

#796

#7960

#7961

#7963

#7966

#7967

#7968

#7969

#797

#7971

#7972

#7973

#7974

#7975

#7976

#7977

#7978

#7979

#7980

#7981

#7982

#7984

#7985

#7986

#7987

#7988

#7989

#7993

#7994

#7995

#7996

#7997

#7998

#7999

#800

#8002

#8003

#8004

#8005

#8006

#8007

#8008

#8011

#8012

#8013

#8020

#8021

#8025

#8026

#8027

#8028

#8029

#8031

#8032

#8033

#8034

#8037

#8038

#8039

#8040

#8043

#8044

#8046

#8047

#8048

#805

#8050

#8060

#8061

#8066

#8070

#8072

#8073

#8077

#8078

#8080

#8081

#8082

#8083

#8084

#8085

#8086

#8088

#8091

#8092

#8093

#8094

#8095

#8098

#81

#8101

#8112

#8113

#8115

#8118

#8119

#8120

#8122

#8123

#8124

#8125

#8126

#8127

#8128

#8129

#8130

#8132

#8133

#8135

#8137

#8138

#8140

#8141

#8143

#8144

#8146

#8147

#8148

#8150

#8152

#8158

#8159

#8160

#8162

#8163

#8166

#8167

#8168

#8171

#8174

#8175

#8176

#8177

#8178

#8179

#8182

#8187

#8189

#8190

#8191

#8192

#8193

#8196

#8197

#8198

#8199

#8201

#8202

#8203

#8204

#8206

#8207

#8209

#8211

#8213

#8214

#8215

#8217

#8218

#8219

#8220

#8221

#8222

#8225

#8226

#8227

#8228

#8229

#8231

#8232

#8233

#8235

#8236

#8238

#8239

#8240

#8241

#8243

#8245

#8246

#8247

#8249

#8251

#8253

#8255

#8256

#8257

#8258

#8259

#8260

#8261

#8263

#8264

#8266

#8268

#8269

#8270

#8271

#8272

#8273

#8275

#8276

#8278

#8279

#8280

#8284

#8285

#8286

#8289

#829

#8290

#8293

#8294

#8295

#8296

#8300

#8302

#8304

#8305

#8306

#8307

#8308

#8309

#8310

#8311

#8313

#8315

#8317

#8321

#8322

#8323

#8325

#8326

#8327

#833

#8331

#8332

#8334

#8336

#8337

#8339

#8340

#8342

#8343

#8347

#8349

#8350

#8351

#8352

#8358

#8359

#8360

#8378

#8379

#838

#8380

#8381

#8382

#8383

#8384

#8385

#8386

#8387

#8388

#8389

#8390

#8391

#8398

#8399

#8401

#8402

#8403

#8404

#8405

#841

#8410

#8416

#8419

#8420

#8425

#8426

#8427

#8428

#8432

#8438

#8439

#8440

#8441

#8442

#8445

#8447

#8448

#8455

#8461

#8462

#8463

#8464

#8465

#8466

#8467

#8470

#8474

#8475

#8476

#8481

#8482

#8483

#8484

#8485

#849

#8490

#8491

#8494

#8498

#8499

#85

#8500

#8507

#8508

#8509

#8510

#8513

#8515

#8518

#8519

#8520

#8521

#8522

#8527

#8528

#853

#8531

#8535

#8538

#854

#8541

#8542

#8543

#8547

#8548

#8554

#8556

#8559

#8560

#8561

#8566

#8567

#8568

#8569

#857

#8570

#8573

#8574

#8577

#8579

#8580

#8583

#8584

#8585

#8588

#8589

#8590

#8591

#8594

#8595

#8597

#8599

#8600

#8602

#8603

#8611

#8623

#8624

#8626

#8631

#8633

#8637

#8638

#8641

#8642

#8645

#8646

#8647

#8650

#8651

#8654

#8655

#8656

#8657

#8658

#8659

#8660

#8661

#8662

#8664

#8667

#8668

#8671

#8673

#8677

#8678

#8681

#8682

#8683

#8686

#869

#8691

#8693

#8694

#8695

#8696

#8699

#87

#8700

#8702

#8703

#8706

#8710

#8711

#8712

#8713

#8714

#8715

#8722

#8725

#8726

#8727

#8728

#8729

#8730

#8735

#8736

#8737

#8741

#8742

#8743

#8744

#8745

#8746

#8747

#8748

#8749

#8752

#8753

#8755

#8756

#8758

#8760

#8761

#8762

#8765

#8766

#8767

#8770

#8774

#8776

#8779

#8780

#8781

#8782

#8785

#8787

#8788

#8789

#8792

#8793

#8794

#8801

#8802

#8803

#8805

#8806

#8807

#8808

#8809

#881

#8810

#8813

#8814

#8815

#882

#8820

#8821

#8824

#8825

#8827

#8828

#8829

#8833

#8834

#8835

#8836

#8837

#8838

#8839

#8844

#8845

#8846

#8847

#8848

#8849

#885

#8851

#8853

#8854

#8856

#8859

#8860

#8863

#8869

#8870

#8871

#8872

#8873

#8874

#8875

#8877

#8878

#8896

#8897

#8898

#8900

#8904

#8905

#8909

#8910

#8911

#8912

#8913

#8914

#8918

#8919

#8920

#8921

#8922

#8923

#8924

#8925

#8927

#8928

#8929

#8930

#8931

#8932

#8933

#8935

#8937

#8938

#8942

#8943

#8944

#8945

#8946

#8948

#8949

#8953

#8954

#8955

#8959

#8960

#8963

#8967

#8968

#8969

#8972

#8977

#8978

#8979

#8982

#8983

#8984

#8988

#8989

#8993

#8994

#8995

#9000

#9001

#9003

#9004

#9006

#9007

#9014

#9015

#9016

#9017

#9018

#9020

#9024

#9025

#9026

#9027

#9028

#9029

#9037

#9038

#9040

#9041

#9042

#9045

#9046

#9047

#9048

#9051

#9053

#9059

#9062

#9064

#9066

#9068

#9069

#907

#9070

#9073

#9075

#9076

#908

#9081

#9087

#9090

#9092

#9095

#9097

#9098

#9099

#910

#9106

#9107

#9109

#9110

#9111

#9112

#9113

#9115

#9116

#9124

#9125

#9129

#9130

#9143

#9150

#9153

#9154

#9155

#9156

#9157

#9165

#9173

#9174

#9175

#9176

#9179

#9180

#9181

#9182

#9183

#9184

#9185

#9186

#9192

#9194

#9195

#9198

#92

#9200

#9204

#9205

#921

#9210

#9215

#9216

#922

#9221

#9222

#9228

#923

#9235

#924

#9241

#9242

#9245

#9246

#9249

#925

#9250

#9253

#9254

#9259

#926

#9260

#9266

#9267

#9268

#9269

#927

#9272

#9275

#9277

#9284

#9290

#9296

#9297

#9298

#9299

#9300

#9302

#9303

#9313

#9320

#9336

#9338

#9343

#9349

#9350

#9352

#9357

#9358

#9359

#936

#9362

#937

#9375

#9376

#938

#9383

#9384

#9390

#9391

#9397

#94

#940

#9405

#9408

#941

#9411

#9413

#9414

#9415

#942

#9423

#9424

#9427

#9432

#9433

#9454

#9461

#9465

#9475

#9476

#9481

#9483

#9489

#9496

#9498

#9500

#9502

#9503

#9507

#9508

#9511

#9512

#9513

#9514

#9515

#9518

#9519

#9523

#9526

#9527

#9529

#9530

#9531

#954

#9547

#9563

#9568

#9570

#9571

#9572

#9577

#9584

#9586

#9587

#9588

#9589

#9590

#9591

#9597

#9607

#9620

#9621

#9624

#9628

#9629

#9630

#9636

#9637

#9639

#9644

#9646

#9647

#9649

#9650

#9653

#9654

#9659

#9660

#9661

#9668

#9669

#9687

#9688

#969

#9692

#9694

#9695

#9696

#9697

#97

#9702

#9704

#9709

#9711

#9712

#9714

#9715

#9716

#9720

#9721

#9722

#9729

#9732

#9733

#9734

#9735

#9736

#9737

#9744

#9745

#9746

#9747

#9748

#9767

#9768

#9769

#9770

#9771

#9772

#9773

#9776

#9777

#9782

#9783

#9785

#9787

#9790

#9796

#9798

#980

#9800

#9803

#9804

#9808

#981

#9811

#9814

#9815

#9816

#982

#9823

#9824

#9825

#9827

#9828

#9829

#983

#9833

#9834

#9838

#984

#9840

#9856

#9857

#9858

#9860

#9868

#9869

#9871

#9872

#9873

#9874

#9875

#9879

#988

#9881

#9882

#9883

#9884

#9891

#9892

#9893

#9899

#9900

#9901

#9902

#9903

#9904

#9906

#9907

#9908

#9909

#9910

#9911

#9913

#9914

#9915

#9916

#9917

#992

#9923

#9924

#9925

#993

#9931

#9932

#9933

#9934

#9935

#9936

#9939

#9940

#9941

#9942

#9944

#995

#9954

#9955

#9956

#9957

#9958

#9959

#9960

#9961

#9962

#9963

#9964

#9965

#9966

#9969

#9970

#9971

#9973

#9976

#9977

#9978

#9979

#9982

#9983

#9984

#9986

#9987

#999

#9990

#9991

#9992

#9996

#9999

Nightly

Z3-4.8.5

last-pure-pure

last-pure-unstable

z3-4.1.1

z3-4.10.0

z3-4.10.1

z3-4.10.2

z3-4.11.0

z3-4.11.2

z3-4.12.0

z3-4.12.1

z3-4.12.2

z3-4.12.3

z3-4.12.4

z3-4.12.5

z3-4.12.6

z3-4.13.0

z3-4.13.2

z3-4.13.3

z3-4.13.4

z3-4.14.0

z3-4.14.1

z3-4.15.0

z3-4.15.1

z3-4.15.2

z3-4.15.3

z3-4.15.4

z3-4.15.5

z3-4.15.6

z3-4.15.7

z3-4.15.8

z3-4.16.0

z3-4.3.0

z3-4.3.1

z3-4.3.2

z3-4.4.0

z3-4.4.1

z3-4.5.0

z3-4.6.0

z3-4.7.1

z3-4.8.1

z3-4.8.10

z3-4.8.11

z3-4.8.12

z3-4.8.13

z3-4.8.14

z3-4.8.15

z3-4.8.16

z3-4.8.17

z3-4.8.3

z3-4.8.4

z3-4.8.6

z3-4.8.7

z3-4.8.8

z3-4.8.9

z3-4.9.0

z3-4.9.1

z3-5.0.0

0843e002b9 Gate the length-residue axiom on what it costs to materialize a length term seq-monadic-sl Margus Veanes 2026-08-09 19:16:27 -07:00
10603d3497

Fix assertion violation in lp_bound_propagator for columns with non-zero delta (#10438) master Nightly Copilot 2026-08-09 18:32:16 -07:00
a72224ccd3

Merge 585d7e328d into 27260ca6da Nikolaj Bjorner 2026-08-09 17:16:32 -07:00
e8e8ae307a

Merge 59d9cc9f02 into 27260ca6da Nikolaj Bjorner 2026-08-10 00:15:38 +00:00
59d9cc9f02

Fix MacOS build: move tst_lp_dio test to top-level src/test dir fix-10417 copilot-swe-agent[bot] 2026-08-10 00:15:34 +00:00
585d7e328d seq_monadic: track unsat core inline during search, drop deletion-based minimization seq-monidic-core Nikolaj Bjorner 2026-08-09 17:15:10 -07:00
86663abb4e Merge master into assertion violation fix Nikolaj Bjorner 2026-08-09 16:58:07 -07:00
97fad0e177

Update lp_bound_propagator.h Nikolaj Bjorner 2026-08-09 16:55:38 -07:00
27260ca6da

Avoid spurious LP debug assertion in optimize by checking constraints in infinitesimal space (#10467) Copilot 2026-08-09 16:30:54 -07:00
15010422f4 fix #10435 - inverted path index may reinsert the same enode repeatedly into the candidate set for instantiation. This caused the overflow as the candidates vector grew beyond the footprint of number of enodes created. A way to address this is to compress the candidates set. We use periodic compression to pay amortized constant cost for compression. Nikolaj Bjorner 2026-08-09 16:25:33 -07:00
cb4d923fcb Add a semilinear length abstraction for regexes and feed it to arithmetic Margus Veanes 2026-08-09 14:37:43 -07:00
1006fdd144 Made c3 modular c3 CEisenhofer 2026-08-09 14:09:20 -07:00
6e11c7f9fc Cleanup CEisenhofer 2026-08-09 13:39:27 -07:00
576b08d9ea

Fix LP debug constraint check for infinitesimal models copilot-swe-agent[bot] 2026-08-09 20:14:18 +00:00
939ba4392a

Enable monadic regex solver by default (#10466) Nikolaj Bjorner 2026-08-09 12:59:36 -07:00
f66fb62671

Merge 44d1b9ca38 into 134cf5f8a6 Nikolaj Bjorner 2026-08-09 19:57:09 +00:00
44d1b9ca38 Use portfolio search for monadic regex constraints seq-dnf-opt Nikolaj Bjorner 2026-08-09 12:57:00 -07:00
134cf5f8a6 Remove unused state graph utility Nikolaj Bjorner 2026-08-09 12:53:50 -07:00
b0f406b0e7

[code-simplifier] Code Simplification - 2026-08-09 (#10468) Nikolaj Bjorner 2026-08-09 12:52:31 -07:00
cdc0c66eb2

Initial plan copilot-swe-agent[bot] 2026-08-09 19:51:12 +00:00
9c8e3316d0 Add fallbacks for exhaustive switches Nikolaj Bjorner 2026-08-09 12:46:10 -07:00
f83dd8f5bd Enable monadic regex solver by default Nikolaj Bjorner 2026-08-09 12:24:37 -07:00
0bdbd2a1b9

Merge 70b2a69559 into 466a5620e1 Nikolaj Bjorner 2026-08-09 19:23:11 +00:00
70b2a69559

Fix min_length calculation using max_length seq-length-lookahead Nikolaj Bjorner 2026-08-09 12:23:08 -07:00
a2f99131e9

Fix min_length calculation for target state Nikolaj Bjorner 2026-08-09 11:43:52 -07:00
3e0d131703 Refactor variable minimum length insertion Nikolaj Bjorner 2026-08-09 10:05:02 -07:00
d6d74d0f33 Merge branch 'seq-dnf-opt' into c3 CEisenhofer 2026-08-09 10:02:21 -07:00
6437a11c73 Code cleanup Added "Z3 resource check" in-between finalize is not relevant anymore CEisenhofer 2026-08-09 09:40:30 -07:00
3db13b1911 Use monadic atom buckets for length pruning Nikolaj Bjorner 2026-08-09 09:24:07 -07:00
6c1c51c20d

Merge 06f458c5a3 into 466a5620e1 1sgtpepper 2026-08-09 15:31:52 +00:00
06f458c5a3

fpa: convert underflow carry to predicate 1sgtpepper 2026-08-09 23:31:45 +08:00
ad741cb424

Merge 6f642509d4 into 466a5620e1 Copilot 2026-08-09 20:54:28 +08:00
30cd295a53

fpa: guard generic round shift widths 1sgtpepper 2026-08-09 19:30:34 +08:00
061d9c64f3

fpa: preserve signed shift-count semantics 1sgtpepper 2026-08-09 13:06:54 +08:00
2f811a5121

fpa: document bounded round shift counts 1sgtpepper 2026-08-09 12:51:53 +08:00
b1eb1a17a7

fpa: widen round shift-count cap 1sgtpepper 2026-08-09 12:49:10 +08:00
a3e6acf554

fpa: lower local underflow result as fields 1sgtpepper 2026-08-09 11:08:47 +08:00
9353479c0a

fpa: clarify deep underflow ownership 1sgtpepper 2026-08-09 10:46:51 +08:00
024747d80e

fpa: remove redundant underflow width alias 1sgtpepper 2026-08-09 10:42:59 +08:00
f53309c7bc

fpa: fix local underflow expression plumbing 1sgtpepper 2026-08-09 10:31:11 +08:00
adccd43aee

fpa: round deep underflow in division 1sgtpepper 2026-08-09 10:28:04 +08:00
3babc666bf

Simplify nested ternary operators in seq_monadic and seq_regex_live github-actions[bot] 2026-08-09 04:04:40 +00:00
84c77dc1ae Refine sequence membership length pruning Nikolaj Bjorner 2026-08-08 19:42:33 -07:00
1d2fc72962 Prune impossible sequence memberships by length Nikolaj Bjorner 2026-08-08 19:35:01 -07:00
1a13bb9bce

fpa: size local leading-zero count independently 1sgtpepper 2026-08-09 09:45:03 +08:00
bb5156d0c3

fpa: document round leading-zero ownership 1sgtpepper 2026-08-09 09:16:37 +08:00
572454faec

Merge bcbe6acc68 into 466a5620e1 1sgtpepper 2026-08-09 10:11:40 +09:00
a154511231

fpa: keep shared round arithmetic operation-independent 1sgtpepper 2026-08-09 09:09:47 +08:00
165cd272e1

fpa: keep wide division exponents local to rounding 1sgtpepper 2026-08-09 09:03:31 +08:00
c7562fb26e

Support division with wider exponents 1sgtpepper 2026-07-29 13:53:22 +08:00
19595435d4

fpa: preserve standard division lowering 1sgtpepper 2026-07-28 22:36:30 +08:00
4c965a8cad

fpa: keep division normalization local 1sgtpepper 2026-07-28 22:32:05 +08:00
8d04196a59

Fix floating-point division normalization 1sgtpepper 2026-07-24 15:58:47 +08:00
bd080e1709

Merge 4bb3d74d61 into 466a5620e1 Clemens Eisenhofer 2026-08-09 00:15:02 +00:00
92bd822105

Merge branch 'master' into seq-length-lookahead Nikolaj Bjorner 2026-08-08 16:20:59 -07:00
466a5620e1

Merge build warning fixes by davedets into Master (#10460) Nikolaj Bjorner 2026-08-08 16:17:39 -07:00
f805b557d2

Merge branch 'Z3Prover:master' into master davedets 2026-08-08 16:14:54 -07:00
3bf54ebfdc

Merge 0ce42a48c8 into e7b7d85d23 Nikolaj Bjorner 2026-08-08 22:40:22 +00:00
0ce42a48c8 Fix monomial bounds unit test fixture arith-round-robin Nikolaj Bjorner 2026-08-08 15:40:13 -07:00
0cd13b0ee0 Merge remote-tracking branch 'origin/seq-dnf-opt' into c3 CEisenhofer 2026-08-08 14:58:52 -07:00
9f242f7e0e

Fix GCC exhaustive switch returns copilot-swe-agent[bot] 2026-08-08 21:56:54 +00:00
69430bd164 manual edits Nikolaj Bjorner 2026-08-08 14:55:09 -07:00
e7b7d85d23 Move nonlinear parameter check into monomial bounds Lev Nachmanson 2026-08-04 13:35:04 -07:00
953f85e1ab nla: re-linearize violated monomials with fixed factors at final check Lev Nachmanson 2026-08-03 10:40:14 -07:00
13d6ab4fbd Merge remote-tracking branch 'origin/master' into c3 CEisenhofer 2026-08-08 14:40:03 -07:00
18f1779e1c Merge branch 'master' of https://github.com/davedets/z3 David Detlefs 2026-08-08 13:57:05 -07:00
afca04e432 Add non-Clang definition of a macro. David Detlefs 2026-08-08 13:56:14 -07:00
d0d79aa13c Update README workflow status badges (#10456) Copilot 2026-08-07 22:09:32 -07:00
ba2e1b8f44 remove stale workflows Nikolaj Bjorner 2026-08-07 21:49:37 -07:00
5e78cd6374 Live-state traversal and interval-refinement product for seq_monadic, minus the postponed prunes (#10455) Margus Veanes 2026-08-07 21:39:20 -07:00
c04e75d442 Fix high-confidence clang-tidy warnings (#10451) Nikolaj Bjorner 2026-08-07 15:49:47 -07:00
0395c29b3a

Merge davedets/master into Detlefs (#10459) Copilot 2026-08-08 13:51:29 -07:00
f3f3daad18

Align imported switch indentation copilot-swe-agent[bot] 2026-08-08 20:43:16 +00:00
9577466d4d

Correct imported warning handling copilot-swe-agent[bot] 2026-08-08 20:42:40 +00:00
8e64ac9f42

Fix imported indentation copilot-swe-agent[bot] 2026-08-08 20:41:52 +00:00
5bafdc021f

Preserve arithmetic solver fallback copilot-swe-agent[bot] 2026-08-08 20:41:10 +00:00
279d0455c3

Fix non-Clang warning macro copilot-swe-agent[bot] 2026-08-08 20:25:49 +00:00
33f88a378f

Merge davedets/master into Detlefs Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> copilot-swe-agent[bot] 2026-08-08 20:21:34 +00:00
cf47297594 Recalibrate the seq_monadic work budget for the interval-refinement product c3-budget Margus Veanes 2026-08-08 12:59:04 -07:00
a9894be876 Recalibrate the seq_monadic work budget for the interval-refinement product seq-monadic-budget Margus Veanes 2026-08-08 12:59:04 -07:00
e9c917b4c5

Merge branch 'master' into master copilot/davedets-master-to-detlefs davedets 2026-08-08 09:56:28 -07:00
8766b939f1 Add a default back in for a case where gcc (erroneously) claims control flow reaches end without return. Must also locally disable the clang covered-switch-default warning. David Detlefs 2026-08-08 09:44:08 -07:00
adb562e4f3 Merge master into c3: live-state traversal + interval-refinement product for seq_monadic c3-merge-master Margus Veanes 2026-08-07 23:48:20 -07:00
40953fa703

Update README workflow status badges (#10456) Copilot 2026-08-07 22:09:32 -07:00
fc4ee2567f

Update README workflow ribbons copilot-swe-agent[bot] 2026-08-08 05:03:55 +00:00
13eed1cfed Merge master into seq-dnf-opt Nikolaj Bjorner 2026-08-07 21:53:15 -07:00
009f3c1ae6 remove stale workflows Nikolaj Bjorner 2026-08-07 21:49:37 -07:00
501dca9403 remove stale workflows optimize-nl-bounds Nikolaj Bjorner 2026-08-07 21:48:33 -07:00
9866fee194

Live-state traversal and interval-refinement product for seq_monadic, minus the postponed prunes (#10455) Margus Veanes 2026-08-07 21:39:20 -07:00
1fea78d5d1 Emit the root first when enumerating live states Margus Veanes 2026-08-07 18:33:07 -07:00
34b0f80f8d Address arithmetic round-robin review Nikolaj Bjorner 2026-08-07 17:04:24 -07:00
e1b3dc9af0 Report interned live-state count in the monadic state display veanes 2026-08-07 16:32:32 -07:00
6d29111ddc Fix arithmetic round-robin regressions Nikolaj Bjorner 2026-08-07 16:22:15 -07:00
d67bbfab6e Build the seq_monadic product from interval refinement instead of a cartesian product (#10384) Margus Veanes 2026-08-04 15:00:21 -07:00
42e82f3e80 Consume live states lazily in dfs_atoms (#10381) Margus Veanes 2026-08-04 14:59:48 -07:00
63ad8f9447 Add lazy regex live-state traversal Nikolaj Bjorner 2026-08-03 15:57:08 -07:00
4e0ec5d01b

Fix high-confidence clang-tidy warnings (#10451) Nikolaj Bjorner 2026-08-07 15:49:47 -07:00
49dccf3d64 Round-robin arithmetic final checks Nikolaj Bjorner 2026-08-07 15:14:58 -07:00
00245058f0 Delete all the default switch cases shown unnecessary by clang's -Wcovered-switch-default. David Detlefs 2026-08-07 15:14:54 -07:00
7c5f5c9842

Merge branch 'Z3Prover:master' into master davedets 2026-08-07 14:51:17 -07:00