Index of /trunk/examples/lassos
Name Last modified Size Description
Parent Directory -
website/ 2015-10-08 03:44 -
uninterpreted_functions/ 2016-10-22 08:47 -
regression/ 2024-10-12 21:50 -
arrays/ 2017-11-16 06:20 -
ZhuGuang.bpl 2015-10-08 03:44 385
ZenoWithoutDivision.bpl 2015-10-08 03:44 615
yPositive-SIscaled75.bpl 2015-10-08 03:44 3.8K
yPositive-SIscaled50.bpl 2015-10-08 03:44 2.6K
yPositive-SIscaled100.bpl 2015-10-08 03:44 5.1K
yPositive-SIscaled.py 2015-10-08 03:44 853
yPositive-MixedIntReal.bpl 2015-10-08 03:44 598
Wellington.bpl 2015-10-08 03:44 527
WaldkirchWithIrrelevantNotequals.bpl 2015-10-08 03:44 636
WaldkirchWithCruft.bpl 2015-10-08 03:44 398
WaldkirchSuggental.bpl 2015-10-08 03:44 423
WaldkirchSiensbach.bpl 2015-10-08 03:44 296
WaldkirchNegativeBound.bpl 2015-10-08 03:44 279
Waldkirch.c 2015-10-08 03:44 158
Vienna.c 2015-10-08 03:44 727
UnboundedDecrease.bpl 2015-10-08 03:44 487
ThunPower2.bpl 2015-10-08 03:44 402
Thun.bpl 2015-10-08 03:44 696
SyntaxSupportUserDefinedTypes01.bpl 2015-10-08 03:44 230
SyntaxSupportMixedIntReal2.bpl 2023-03-16 09:31 349
SyntaxSupportFunctions01.bpl 2016-09-14 22:32 269
SyntaxSupportConst03.bpl 2015-10-08 03:44 280
SyntaxSupportBitwiseOperations01.c 2016-09-14 22:32 164
Stockholm.bpl 2015-10-08 03:44 299
simple-scaled250.bpl 2015-10-08 03:44 16K
simple-scaled200.bpl 2015-10-08 03:44 13K
simple-scaled100.bpl 2015-10-08 03:44 6.1K
simple-scaled.py 2015-10-08 03:44 1.0K
Selestat.bpl 2015-10-08 03:44 215
Schaafheim_false-termination.c 2016-08-03 17:34 321
SantaBarbara02.bpl 2015-10-08 03:44 357
SantaBarbara01.bpl 2015-10-08 03:44 611
SanDiego.bpl 2015-10-08 03:44 570
Rotation02.bpl 2015-10-08 03:44 316
RebihaMouraMatringe-CoRR2014-Example1.1.bpl 2015-10-08 03:44 551
Ramciel.bpl 2015-10-08 03:44 343
Pure2Phase.bpl 2015-10-08 03:44 366
PuertoRico.bpl 2015-10-08 03:44 274
PodelskiRybalchenko-VMCAI2004-Ex2.bpl 2015-10-08 03:44 606
OpposedDisjuncts.bpl 2015-10-08 03:44 413
Nyala-TwoLex.bpl 2015-10-08 03:44 447
NonTerminationSimple8.bpl 2015-10-08 03:44 333
NonTerminationSimple7.bpl 2015-10-08 03:44 204
NonTerminationSimple6.bpl 2015-10-08 03:44 204
NonTerminationSimple4.bpl 2015-10-08 03:44 246
NonTerminationSimple.bpl 2015-10-08 03:44 255
NonTerminationSameEigenvalues.bpl 2018-04-05 15:06 362
NonTerminationRotation.bpl 2015-10-08 03:44 261
NonTerminationReal.bpl 2015-10-08 03:44 192
NonTerminationProjection01.bpl 2018-03-23 10:46 351
NonTerminationPartitioned.bpl 2015-10-08 03:44 404
NonTerminationOverReals.bpl 2015-10-08 03:44 343
NonterminationNilpotentComponents.bpl 2016-01-12 18:58 404
NonTerminationMykonos01.bpl 2021-02-19 15:38 356
NonTerminationFixedPoint.bpl 2015-10-08 03:44 260
NonterminationDifficult12_LeMans.bpl 2016-09-14 22:32 267
NonterminationDifficult11_UpperTriangularDifferentEigenvalue.bpl 2016-01-12 18:58 289
NonterminationDifficult10_0FTW.bpl 2015-12-16 14:07 442
NonterminationDifficult09_Wolfsburg.bpl 2015-10-08 03:44 477
NonterminationDifficult08_ThreeHomogenized.bpl 2015-12-21 15:46 264
NonterminationDifficult08_Int.bpl 2015-12-16 14:07 614
NonterminationDifficult08.bpl 2015-10-08 03:44 363
NonterminationDifficult07_Hanoi_plus.bpl 2015-10-08 03:44 421
NonterminationDifficult06.bpl 2015-10-08 03:44 437
NonterminationDifficult05_ComplexEigenvalues.bpl 2015-10-08 03:44 382
NonterminationDifficult04.bpl 2015-10-08 03:44 461
NonterminationDifficult03.bpl 2015-10-08 03:44 522
NonterminationDifficult02.bpl 2015-10-08 03:44 313
NonterminationDifficult01.bpl 2015-10-08 03:44 283
NonTerminationChangeOfBasisDemonstration01.bpl 2018-03-14 14:12 276
NonterminationCAV_03.bpl 2016-02-03 18:56 222
NonterminationCAV_02.bpl 2016-02-03 18:56 222
NonterminationCAV_01.bpl 2016-02-03 18:56 219
NonTermination3.bpl 2015-10-08 03:44 238
NonTermination2.bpl 2015-10-08 03:44 279
NonTermination1.bpl 2015-10-08 03:44 231
NewYork01.bpl 2021-02-19 15:38 344
Nangang-FakeDisjunction.bpl 2017-11-16 06:20 1.8K
Mysore2.bpl 2015-10-08 03:44 277
Mysore.bpl 2015-10-08 03:44 329
MunichWithInvariant.bpl 2015-12-16 14:07 363
Munich.bpl 2015-12-16 14:07 334
MultiphaseRotation53nondet.bpl 2015-10-08 03:44 694
MultiphaseRotation53.bpl 2015-10-08 03:44 529
MultiphaseRotation180_2.bpl 2015-10-08 03:44 701
MultiphaseRotation180.bpl 2015-10-08 03:44 558
MultiphaseOnlyInThesis.c 2015-10-08 03:44 1.1K
MultiPhase1.bpl 2015-10-08 03:44 454
MultiLex.bpl 2015-10-08 03:44 293
Moscow.bpl 2015-10-08 03:44 276
Modulo.bpl 2015-10-08 03:44 193
MenloPark2.bpl 2015-10-08 03:44 791
MenloPark.bpl 2015-10-08 03:44 482
Madrid.bpl 2015-10-08 03:44 764
LTL_Coolant_Nonterminating01.bpl 2015-10-08 03:44 780
LoopUnsat.bpl 2015-10-08 03:44 272
Lobnya-Boolean.bpl 2015-10-08 03:44 290
Lobnya-Boolean-Reordered.bpl 2015-10-08 03:44 297
linRakWithNonTrivialSI01.bpl 2015-10-08 03:44 331
LexConj-Ben-Amram.bpl 2015-10-08 03:44 303
Konstanz.bpl 2016-08-03 17:34 761
Kinshasa.bpl 2015-10-08 03:44 207
Khartoum.bpl 2015-10-08 03:44 231
IntegerVsRealSimple.bpl 2015-10-08 03:44 294
IncreasingSI.bpl 2015-10-08 03:44 339
Hammereisenbach-AlternatingBranches_false-termination.c 2016-08-03 17:34 347
GulwaniResetBranchOnly.bpl 2015-10-08 03:44 553
Gulwani.bpl 2015-10-08 03:44 504
Gothenburg.bpl 2015-10-08 03:44 380
Glastonbury.bpl 2015-10-08 03:44 454
GcdNew.bpl 2015-10-08 03:44 474
Gcd_havoc.bpl 2015-10-08 03:44 592
Gcd.bpl 2015-10-08 03:44 397
Garmisch.bpl 2015-10-08 03:44 715
FourPhase.bpl 2015-10-08 03:44 611
ExponentialGrowth.bpl 2015-10-08 03:44 540
Edmonton.bpl 2015-10-08 03:44 427
Dresden.bpl 2015-10-08 03:44 604
DivisionTerminating.bpl 2015-10-08 03:44 253
Division.bpl 2015-10-08 03:44 298
Dhaka.bpl 2015-10-08 03:44 400
DecreasingInvariant.bpl 2015-10-08 03:44 368
Damaskus.bpl 2015-10-08 03:44 260
CrazySpirals.bpl 2015-10-08 03:44 834
CopenhagenYis0.bpl 2015-10-08 03:44 239
CopenhagenWithTmp.bpl 2015-10-08 03:44 277
CooperatingT2_consts1.bpl 2015-10-08 03:44 519
ConjunctiveLoopWithoutNestedRF.bpl 2015-10-08 03:44 725
ConjunctiveLassoDifficultTerminating.bpl 2015-10-08 03:44 587
ConjunctiveLassoDifficultNonterminating.bpl 2015-10-08 03:44 590
Collatz.bpl 2015-10-08 03:44 277
Cairo2.bpl 2015-10-08 03:44 229
Cairo.bpl 2015-10-08 03:44 358
Braverman-2006CAV-Ex1-int.bpl 2015-10-08 03:44 385
BradleyMannaSipma-2005ICALP-Fig2.bpl 2015-10-08 03:44 1.3K
BradleyMannaSipma-2005ICALP-Fig1.bpl 2015-10-08 03:44 732
BradleyMannaSipma-2005ICALP-Fig1-deterministic.bpl 2015-10-08 03:44 626
bound-scaled600.bpl 2015-10-08 03:44 15K
bound-scaled400.bpl 2015-10-08 03:44 10K
bound-scaled200.bpl 2015-10-08 03:44 4.9K
bound-scaled.py 2015-10-08 03:44 730
Boulder.bpl 2015-10-08 03:44 616
BooleanSwap.bpl 2015-10-08 03:44 324
Benghazi.bpl 2015-10-08 03:44 511
BenAmram-2010LMCS-Ex2.3.bpl 2015-10-08 03:44 535
Barcelona.bpl 2015-10-08 03:44 413
BangaloreStrictIneq.bpl 2015-10-08 03:44 365
Bangalore3.bpl 2015-10-08 03:44 595
Bangalore2.bpl 2015-10-08 03:44 256
Bangalore.c 2015-10-08 03:44 266
Bangalore.bpl 2015-10-08 03:44 298
5Phase.bpl 2015-10-08 03:44 348
4Phase.bpl 2015-10-08 03:44 335
4NestedWith3Variables.bpl 2015-10-08 03:44 737
3Phase.bpl 2015-10-08 03:44 451
3Parallel.bpl 2015-10-08 03:44 378
2013POPL-BenAmGen-Ex4.2.bpl 2015-10-08 03:44 736
2013POPL-BenAmGen-Ex3.6.bpl 2015-10-08 03:44 384
2013POPL-BenAmGen-Ex3.20.bpl 2015-10-08 03:44 469
2013POPL-BenAmGen-Ex3.20-Real.bpl 2015-10-08 03:44 505