-
Notifications
You must be signed in to change notification settings - Fork 3
Expand file tree
/
Copy pathnews.shtml
More file actions
497 lines (484 loc) · 26.9 KB
/
news.shtml
File metadata and controls
497 lines (484 loc) · 26.9 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>SMT-LIB The Satisfiability Modulo Theories Library</title>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<link href="style.css" rel="stylesheet" type="text/css" />
<!-- CuFon: Enables smooth pretty custom font rendering. 100% SEO friendly. To disable, remove this section -->
<script type="text/javascript" src="js/cufon-yui.js"></script>
<script type="text/javascript" src="js/arial.js"></script>
<script type="text/javascript" src="js/cuf_run.js"></script>
<!-- CuFon ends -->
<link href="code-prettify/prettify.css" type="text/css" rel="stylesheet" />
<script src="code-prettify/run_prettify.js?lang=smtlib&skin=desert"></script>
</head>
<body>
<div class="main">
<div class="header">
<div class="header_resize">
<div class="menu_nav">
<ul>
<li><a href="index.shtml">Home</a></li>
<li><a href="about.shtml">About</a></li>
<li class="active"><a href="news.shtml">News</a></li>
<li><a href="standard.shtml">Standard</a></li>
<li><a href="benchmarks.shtml">Benchmarks</a></li>
<li><a href="software.shtml">Software</a></li>
<li><a href="credits.shtml">Credits</a></li>
</ul>
</div>
<div class="clr"></div>
<div class="logo">
<h1><a href="index.shtml">SMT-LIB <br/>
<small>The Satisfiability Modulo Theories Library</small></a>
</h1>
</div>
</div>
</div>
<div class="content">
<div class="content_resize">
<div class="mainbar">
<div class="article">
<h2>News</h2>
<!------------------------------------------------------------------------>
<a name="2025-02-05"></a>
<small>February 5, 2025</small>
<p>
A new release of Version 2.7 of the SMT-LIB reference document
is now available. This release allows polymorphic types in
assertions, and introduces a theory of maps that models
higher-order functions.
</p>
<a name="2024-09-20"></a>
<small>September 20, 2024</small>
<p>
A new release of the SMT-LIB 2.6 reference document
is now available. This is a minor release. The main changes
concern the verbosity of the output.
</p>
<a name="2024-04-02"></a>
<small>April 2, 2024</small>
<p>
Starting today, the benchmark library will no longer be publicly available from the University of Iowa's GitLab server.
Official yearly releases of the library will be available
<a href="https://zenodo.org/communities/smt-lib">Zenodo</a>.
</p>
<a name="2024-02-13"></a>
<small>Feb 13, 2024</small>
<p>
The latest release (2023) of the SMT-LIB benchmark library is now
available on <a href="https://zenodo.org/communities/smt-lib">Zenodo</a> in the form of compressed archives.
</p>
<a name="2021-05-12"></a>
<small>May 12, 2021</small>
<p>
A new release of the the SMT-LIB 2.6 reference document
is now available. This is a minor release addressing a
minor error in the 2021-04-02 release.
</p>
<a name="2021-04-02"></a>
<small>April 2, 2021</small>
<p>
A new release of the the SMT-LIB 2.6 reference document
is now available. This is a minor release addressing a few
errors in the 2017-07-18 release.
</p>
<a name="2020-01-11"></a>
<small>Feb 11, 2020</small>
<p>
A theory of Unicode character strings and regular expressions has been added
to the set of <a href="theories.shtml">SMT-LIB theories</a>.
</p>
<a name="2019-05-09"></a>
<small>May 9, 2019</small>
<p>A new release of the SMT-LIB benchmark library (2019-05-09) is now
available, both on the
<a href="https://clc-gitlab.cs.uiowa.edu:2443/explore/groups">GitLab</a> server and on
<a href="https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=294532">StarExec</a>.
For this release, we have:
<ul>
<li>Added 49,005 new benchmarks in new logics:
non-incremental:
QF_BVFPLRA (1), QF_FPLRA (13), QF_S (1976), QF_SLIA (46,350),
UFDTNIA (1);
incremental:
QF_AUFBVLIA (441), QF_AUFBVNIA (44), QF_UFBVLIA (179).
</li>
<li>Added 17,890 new benchmarks in existing logics:
non-incremental:
FP (2,415), QF_ABV (17), QF_AUFBV (25), QF_BV (1594),
QF_UFBV (10), QF_UFNIA (471), UFDTLIA (24), UFNIA (10,105);
incremental:
QF_ABV (1,257), QF_ABVFP (60), QF_AUFBV (21), QF_BV (1,771),
QF_BVFP (117), QF_UFBV (3).
</li>
<li>Updated statuses of 3039 previously unknown non-incremental
benchmarks (based on the results from 2 or more solvers from SMT-COMP'18).
</li>
<li>Updated 79255 statuses of previously unknown incremental check-sat
calls (based on the results from 2 or more solvers from SMT-COMP'18).
</li>
<li>Removed duplicate benchmarks
</li>
<li>Unified Sage2 and QF_BV benchmark repositories (non-incremental).
</li>
</ul>
GitLab changes:
<ul>
<li>Benchmarks with a size >= 10M are now stored via git LFS. Please
refer to the repository's README on how to check out the repository.
</li>
<li>We unified the Sage2 and QF_BV repositories into one
repository. A fresh checkout is required since the git history of the
repository has been rewritten.
</li>
</ul>
Thank you to the 11 submitters of the new benchmarks:
Thomas Bunk,
Bernhard Gleiss,
Alexandre Gonzalvez,
Matthias Güdemann,
Jie-Hong Roland Jiang,
Makai Mann,
Andres Nötzli,
Mathias Preiner,
Andrew Reynolds,
Clifford Wolf,
Yoni Zohar.
</p>
<!------------------------------------------------------------------------>
<a name="2018-05-20"></a>
<small>May 20, 2018</small>
<p>A new release of the SMT-LIB benchmark library (2018-05-20) is now
available, both on the
<a href="https://clc-gitlab.cs.uiowa.edu:2443/explore/groups">GitLab</a> server and on
<a href="https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=294532">StarExec</a>.
For this release we have:
fixed minor errors in formatting;
removed duplicate benchmarks; updated statuses of 18,739 previously unknown non-incremental
benchmarks (based on the results from 2 or more solvers from SMT-COMP'17);
updated 232,167 statuses of previously unknown incremental check-sat
calls (based on the results from 2 or more solvers from SMT-COMP'17);
added 3,121 new benchmarks in new logics:
(non-incremental: AUFNIA (3),
incremental: QF_ABV (15), QF_AUFBV (10), QF_UF (766), QF_UFBV (2327));
added 7,969 new benchmarks in previous logics:
(non-incremental: AUFLIA (3272), BV (600), NRA (2), QF_ABV (5),
QF_AUFLIA (294), QF_BV (67), QF_LIA (806), QF_NRA (135), QF_UF (807),
QF_UFBV (1193)
- incremental: QF_BV (787), QF_LIA (1)
For details on the changes to SMT-LIB, please check the git logs for <a href="https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-inc
">incremental</a> and <a href="https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks">non-incremental</a> benchmarks.
</p>
<a name="2017-07-18"></a>
<small>July 18, 2017</small>
<p>Version 2.6 of the SMT-LIB standard has been released and is now available in the <a href="language.shtml">Language</a> section.
Its main difference with Version 2.5 is the addition of algebraic datatypes to the language.
See the document for more details.
</p>
<a name="2017-06-08"></a>
<small>June 8, 2017</small>
<p>A new release of the SMT-LIB benchmark library is now available, both on the <a href="https://clc-gitlab.cs.uiowa.edu:2443/explore/groups">GitLab</a> server and on <a href="https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=234826">StarExec</a>. For this release we have fixed minor errors in formatting; removed duplicate benchmarks; updated statuses of 6,492 previously unknown benchmarks based on the results produced by 2 or more solvers from SMT-COMP'16; added new benchmarks in new logics: ABVFP, AUFBVDTLIA, AUFDTLIA, BVFP, FP, QF_ABVFP, QF_DT, UFDT, UFDTLIA (non-incremental) and ABVFP, BV, BVFP, LRA, QF_ABVFP, QF_BVFP, QF_FP (incremental); added new benchmarks in existing logics:
BV, LRA, QF_BV, QF_BVFP, QF_FP, QF_LRA, QF_NIA, QF_NRA, UF (non-incremental) and
QF_BV (incremental).
For details on the changes to SMT-LIB, please check the git logs for the
<a href="https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks">non-incremental</a> and
<a href="https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-inc">incremental</a> benchmarks.
</p>
<a name="2017-06-05"></a>
<small>June 5, 2017</small>
<p>A close-to-final draft of the upcoming version of the SMT-LIB standard, version 2.6, is now available in the <a href="language.shtml">Language</a> section. The most notable new features is the addition of algebraic datatypes to the language.
</p>
<a name="2017-05-30"></a>
<small>May 30, 2017</small>
<p>The discussion list <b>smt-lib@cs.nyu.edu</b> has been decommissioned.
Its archives will remain available at <a href="http://www.cs.nyu.edu/pipermail/smt-lib">http://www.cs.nyu.edu/pipermail/smt-lib</a>.
The new discussion forum for SMT-LIB is now <a href="https://groups.google.com/d/forum/smt-lib">https://groups.google.com/d/forum/smt-lib</a>.
</p>
<a name="2017-04-27"></a>
<small>April 27, 2017</small>
<p>The SMT-LIB benchmark repository is now hosted on the <a href="https://clc-gitlab.cs.uiowa.edu:2443/explore/groups">SMT-LIB GitLab</a> service. See the <a href="benchmarks.shtml">Benchmarks</a> section for more info.
</p>
<a name="2015-06-01"></a>
<p><small>June 1, 2015</small><br> A new release of the SMT-LIB
benchmark library is available on StarExec. Many old benchmarks that
had status "unknown" now have updated statuses of either "sat" or
"unsat". A number of new benchmarks have also been added, both
incremental and non-incremental. Incremental divisions with new
benchmarks are: ALIA, ANIA, LIA, QF_ALIA, QF_ANIA, QF_LIA, QF_NIA, and
QF_UFNIA. Non-incremental divisions with new benchmarks are: LIA, NIA,
QF_ALIA, QF_AUFNIA, QF_LIRA, QF_NIA, QF_NIRA, UFBV, UFLIA, and UFNIA.
Benchmarks can be downloaded directly from StarExec or from a mirror at
<a href="http://www.cs.nyu.edu/~barrett/smtlib/">NYU</a>.
</p>
<a name="2015-05-28"></a>
<p><small>May 28, 2015</small><br>
Version 2.5 of the SMT-LIB standard is out!
It is an extension of Version 2.0 and, with two minor exceptions, it is fully backward compatible with that previous version.
See the <a href="language.shtml">Language</a> section for the reference document.
</p>
<a name="2014-06-11"></a>
<p><small>June 11, 2014</small><br>
For bulk downloads, zip archives containing section of the latest release of the repository (2014-06-03) are also available. See the <a href="benchmarks.shtml">Benchmarks</a> section for further instructions.
</p>
<a name="2014-06-04"></a>
<p><small>June 4, 2014</small><br>
The migration of the benchmark repository to the StarExec service is now complete. See the <a href="benchmarks.shtml">Benchmarks</a> section for instructions on how to access the repository.<br>
The current release, 2014-06-03, has been considerably expanded with new logics and thousands of new benchmarks.
We have also created a few new logics that best describe some sets of benchmarks. As a consequence, a number of old benchmarks have been reclassified accordingly logic-wise.
</p>
<p><small>June 4, 2014</small><br>
We have added a graph in the <a href="logics.shtml">Logics</a> section that illustrates the containment relation between the various SMT-LIB logics.
</p>
<p><small>May 24, 2014</small><br>
A theory of floating point numbers, called <code>FloatingPoint</code>, has
been added to the Theories section.
</p>
<p><small>May 24, 2014</small><br>
A new, completely revamped web site went live today.
</p>
<p><small>June 26, 2013</small><br>
A <code>:value</code> attribute has been defined for the theory <code>FixedSizedBitvectors</code>.
</p>
<p><small>June 26, 2013</small><br>
The theory <code>Fixed_Sized_Bitvectors</code> has been renamed <code>FixedSizedBitvectors</code>, for naming consistency. The logic declarations that refer to that theory have been updated accordingly.
</p>
<p><small>September 9, 2012</small><br>
A new release of the reference of the Version 2.0 reference document has been posted in the Documents section. It contains a few minor fixes and a clarification on the language of a logic.
</p>
<p><small>June 14, 2011</small><br>
The definition of bvsmod in the <code>QF_BV</code> logic has been updated to correct a bug (the definition was incorrect in case the divisor is negative and the dividend is a multiple of the divisor).
</p>
<p><small>June 11, 2011</small><br>
The declarations for the following logics have been added in the Logics section: <code>QF_NRA</code>, <code>QF_UFBV</code>, <code>QF_UFLIA</code>, <code>QF_UF<code>LRA</code>, <code>QF_UF</code>NRA</code>, <code>UFLRA</code>, <code>UFNIA</code>. A couple of them are new. The rest had had benchmarks in the library for a while but their declaration was missing.
</p>
<p><small>June 03, 2011</small><br>
Fixed an error in the declaration of all the logics including the <code>Reals</code> theory (the definition of coefficient in the <code>:extension</code> attribute was missing a case).
</p>
<p><small>June 03, 2011</small><br>
Added a note to the declaration of <code>QF_UFIDL</code>.
</p>
<p><small>June 03, 2011</small><br>
Extended the definition of linear term in the <code>:extension</code> attribute of <code>QF_AUFLIA</code>.
</p>
<p><small>January 18, 2011</small><br>
Links to a set of Java utilities for SMT-LIB 2 scripts has been added in the Utilities section.
</p>
<p><small>January 18, 2011</small><br>
A tutorial, by D. Cok, on the SMT-LIB 2 format has been added in the Documents section.
</p>
<p><small>December 21, 2010</small><br>
A new release of the Version 2.0 reference document has been posted in the Documents section. This is another minor release, fixing a number errors, clarifying the text in a few points, and adjusting the standard in minor ways.
</p>
<p><small>September 1, 2010</small><br>
Section Utilities has been revamped, with the addition of two parsers for SMT-LIB 2.
</p>
<p><small>August 28, 2010</small><br>
A new release of the Version 2.0 reference document has been posted in the Documents section. This is a minor release, fixing a number errors, clarifying the text in a few points, and adjusting the standard in minor ways.
</p>
<p><small>May 4, 2010</small><br>
An initial version of the benchmark repository in the SMT-LIB 2.0 format is now available in the Benchmarks section. Conformance checking is still ongoing, and these benchmarks may be changed to conform to the SMT-LIB 2.0 format.
</p>
<p><small>May 1, 2010</small><br>
A number of theory and logic declarations have been converted from Version 1.2 to Version 2.0 of the SMT-LIB format. They are available in the Theories and Benchmarks sections. More theories and logic declarations will be added in the next few days.
</p>
<p><small>March 30, 2010</small><br>
Version 2.0 of the SMT-LIB format has been released. Its reference document, which supersedes all previous drafts, is now available from the Documents section.
</p>
<p><small>February 10, 2010</small><br>
An updated, almost final draft of the Version 2.0 document is now available in the Documents section.
</p>
<p><small>February 1, 2010</small><br>
A draft of the coming Version 2.0 of the SMT-LIB format is now available in the Documents section.
</p>
<p><small>August 18, 2009</small><br>
A link to Robert Brummayer's SMT debugging utilities has been added in the Utilities section.
</p>
<p><small>July 4, 2009</small><br>
The logic <code>LRA</code>, for (quantified) formulas in linear real arithmetic, has been added.
</p>
<p><small>July 2, 2009</small><br>
Updates and additions to the new 2009 benchmarks have been posted to the SMT-LIB benchmark page. No new benchmarks will be added before SMT-COMP 2009. These benchmarks are in the process of being integrated with the SMT-LIB.
</p>
<p><small>June 25, 2009</small><br>
Three new logics have been added, all having to do with non-linear arithmetic: <code>QF_NIA</code>, <code>QF_UFNRA</code> and <code>UFNIA</code>.
</p>
<p><small>June 3, 2009</small><br>
New benchmarks for 2009 have been posted to the SMT-LIB benchmark page. These benchmarks are in the process of being integrated with the SMT-LIB.
</p>
<p><small>June 5, 2008</small><br>
<code>QF_BV</code>/spear benchmarks were missing the ":formula" attribute. ":formula true" has been added to all of these benchmarks.
</p>
<p><small>June 1, 2008</small><br>
Status and difficulty updates have been done across all benchmarks. Also, 1485 benchmarks were moved from <code>QF_AUFLIA</code> to <code>QF_AX</code>. These benchmarks do not use uninterpreted functions or arithmetic in any meaningful way. The only change needed was to change the sorts from Int to Index/Element in order to fit within the <code>QF_AX</code> logic. Fixed a typo in <code>QF_AUFBV</code>: brummaryerbiere -> brummayerbiere.
</p>
<p><small>May 21, 2008</small><br>
An additional 415 benchmarks have been added to <code>QF_BV</code> in subdirectories uclid/catchconv (the 1 existing benchmark was moved here) and uclid/tcas.
</p>
<p><small>May 20, 2008</small><br>
A total of 66 new benchmarks have been added to <code>QF_BV</code>: 65 in brummayerbiere2 and 1 in uclid.
Minor fixes have been made in <code>QF_UF/eq_diamond</code> and <code>QF_BV/brummayerbiere</code>.
The <code>UFNIA</code> benchmarks have been added as "pending".
</p>
<p><small>May 1, 2008</small><br>
A total of 935 new benchmarks have been added.
<code>QF_AUFBV</code> : 293 in brummayerbiere;
<code>QF_BV</code> : 13 in brummayerbiere;
<code>QF_IDL</code> : 280 in schedulingIDL;
<code>QF_LIA</code> : 294 in rings;
QF_<code>LRA</code> : 42 in miplib;
<code>QF_UFIDL</code> : 13 in bcnscheduling.
</p>
<p><small>April 14, 2008</small><br>
A total of 4731 new benchmarks have been added.
<code>AUFLIA</code> : 32 in sexpr;
<code>AUFLIRA</code> : 198 in peter;
<code>QF_IDL</code> : 248 in parity;
<code>QF_LIA</code> : 2780 in nec-smt;
<code>QF_UF</code> : 100 in eq_diamond;
<code>QF_UFIDL</code> : 19 in mathsat;
<code>QF_UFLIA</code> : 454 in mathsat.
A new category of benchmarks added.
<code>QF_UFLRA</code> : 900 in mathsat.
</p>
<p><small>February 20, 2008</small><br>
All benchmarks have been updated to the version used in SMT COMP 2007.
</p>
<p><small>June 19, 2007</small><br>
Rebuilt the <code>AUFLIA</code> tar file.
</p>
<p><small>June 18, 2007</small><br>
The logic field for the check benchmarks has been updated to always match the division in which the benchmark appears. Additionally, the status and difficulty fields have been updated in some of the benchmarks in <code>QF_BV</code>/tacas07.
</p>
<p><small>June 14, 2007</small><br>
A minor problem with the <code>QF_BV</code>/spear benchmarks has been fixed.
</p>
<p><small>June 12, 2007</small><br>
The new bitvector theories and logics have been posted. Also, a total of 2011 new benchmarks have been added to <code>QF_BV</code> and 8168 new benchmakrs have been added to <code>QF_AUFBV</code>. Some of these have been retranslated from <code>QF_UFBV </code>32. The rest are from various sources and make use of the new theories and logics.
</p>
<p><small>May 17, 2007</small><br>
A set of sample benchmarks have been added to <code>QF_BV</code> and <code>QF_AUFBV</code>.
</p>
<p><small>May 08, 2007</small><br>
A total of 3603 new benchmarks have been added to the set of <code>AUFLIA</code> benchmarks. These are translations of the boogie benchmarks (see http://research.microsoft.com/specsharp/) and an alternative and more complete translation of the simplify benchmarks (in subdirectory simplify2). These were translated by Michal Moskal.
</p>
<p><small>May 1, 2007</small><br>
A total of 1325 new benchmarks have been added to the set of <code>AUFLIRA</code>benchmarks. These are translations of the Caduceus benchmarks provided by Claude Marche using the Why verifiction tool. See http://proval.lri.fr/why-benchmarks.
</p>
<p><small>Movember 20, 2006</small><br>
A total of 6404 new benchmarks have been added to the set of <code>QF_UF</code> benchmarks. These were provided by Volker Sorge and are based on classification of quasi-groups.
</p>
<p><small>November 19, 2006</small><br>
Most of the RTCL benchmarks were moved from <code>QF_LIA</code> to <code>QF_UFIDL</code> because they are a better fit for difference logic than linear arithmetic.
</p>
<p><small>November 19, 2006</small><br>
Some slight modifications were made to a number of the other <code>QF_UFIDL</code> benchmarks to eliminate the use of constructs that technically are not allowed by this logic.
</p>
<p><small>September 1, 2006</small><br>
This web site has now a new url: www.SMT-LIB.org .
</p>
<p><small>August 5, 2006</small><br>
A new version of the SMT-LIB format has been released. Notable changes are the possibility of overloading function and predicate symbols, and the addition of indexed identifiers (see the document).
</p>
<p><small>July 24, 2006</small><br>
A new version of the benchmarks has been released. Some benchmarks have been reclassified, and several more have been added for both new and old logics.
</p>
<p><small>May 11, 2006</small><br>
A theory of bit vectors with size up to 32 bits and a related logic have been added. The logic will be a division in the next SMT-COMP.
</p>
<p><small>17/04/, 2006</small><br>
The SMT-LIB discussion list has moved to a new server.
</p>
<p><small>June 28, 2005</small><br>
A new version of the benchmarks has been released. Some benchmarks have been reclassified, others have been retranslated because they were in an incorrect format. A few more have been added.
</p>
<p><small>April 8, 2005</small><br>
The first set of benchmarks in SMT-LIB format has been added to the Benchmarks section!
</p>
<p><small>April 8, 2005</small><br>
An initial set of SMT-LIB (sub)logic specifications has been released, in the Logics section.
</p>
<p><small>April 8, 2005</small><br>
An initial set of SMT-LIB theory specifications has been released, in the Theories section.
</p>
<p><small>March 18, 2005</small><br>
Version 1.1 of the SMT-LIB standard has been posted, in the Documents section.
</p>
<p><small>October 18, 2004</small><br>
Added link to SMT-COMP'05 in the SMT-COMP section.
</p>
<p><small>September 5, 2004</small><br>
We now have a section of SMT-COMP, the SMT solver competition.
</p>
<p><small>July 27, 2004</small><br>
Updated section on discussion list.
</p>
<p><small>July 27, 2004</small><br>
A new section on the SMT-LIB system competition has been added.
</p>
<p><small>July 26, 2004</small><br>
A couple of sample declarations of theories in SMT-LIB format, Arrays-1 and <code>Reals</code>-1, have been posted in the Documents section.
</p>
<p><small>July 26, 2004</small><br>
Version 1.0 of the SMT-LIB standard has been published! Check out the Documents section of this site.
</p>
<p><small>July 25, 2004</small><br>
The list of SMT solvers in the Solvers section has been updated.
</p>
<p><small>July 24, 2004</small><br>
News page created. Check this page for news on the SMT-LIB initiative and for updates on this website.
</p>
</div>
</div>
<div class="sidebar">
<div class="gadget">
<ul class="sb_menu">
<li><a href="index.shtml">Home</a></li>
<li><a href="about.shtml">About</a></li>
<li><a href="news.shtml">News</a></li>
<li>Standard
<ul class="ex_menu">
<li><a href="language.shtml">Language</a>
<li><a href="theories.shtml">Theories</a>
<li><a href="logics.shtml">Logics</a>
<li><a href="examples.shtml">Examples</a>
</ul>
</li>
<li><a href="benchmarks.shtml">Benchmarks</a></li>
<li>Software
<ul class="ex_menu">
<li><a href="solvers.shtml">Solvers</a></li>
<li><a href="utilities.shtml">Utilities</a></li>
</ul>
</li>
<li><a href="contact.shtml">Contact</a></li>
<li><a href="related.shtml">Related</a></li>
<li><a href="credits.shtml">Credits</a></li>
</ul>
</div>
</div>
</div>
</div>
<div class="clr"></div>
<div class="footer">
<div class="footer_resize">
<p class="lf">
© Copyright The SMT-LIB Initiative <br>
Based on a design by
Blue <a href="http://www.bluewebtemplates.com">Web Templates</a>
</p>
<ul class="fmenu">
<li><a href="index.shtml">Home</a></li>
<li><a href="about.shtml">About</a></li>
<li class="active"><a href="news.shtml">News</a></li>
<li><a href="standard.shtml">Standard</a></li>
<li><a href="benchmarks.shtml">Benchmarks</a></li>
<li><a href="software.shtml">Software</a></li>
<li><a href="credits.shtml">Credits</a></li>
</ul>
<div class="clr"></div>
</div>
</div>
</div>
</body>
</html>