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