-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathchange_history.txt
194 lines (171 loc) · 5.51 KB
/
change_history.txt
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
Note: history only accounts for content changes, not release changes.
2023-11-01
Reference/concrete-syntax.tex
Reference/operational-semantics.tex
Changed verbosity to have no standard default value
Changed default for print-success to be false
2020-08-06
Theories/UnicodeStrings.smt2
Fixed an example in Strings constant definition.
2020-05-20
Logics/QF_BV.smt2
bvxnor is no longer marked as left associative, as that is
inconsistent with its meaning as the negation of bvxor.
Theories/FixedSizeBitVectors.smt2
Fixed minor typo
2020-02-09
Theories/UnicodeStrings.smt2
Mostly layout fixes in UnicodeStrings
2020-02-01
Theories/UnicodeStrings.smt2
To stable version. Comments are fixed. A few functions are added.
2019-05-07
Theories/UnicodeStrings.smt2
Draft 2.1
Fixed a few typos in UnicodeStrings and changed names from hyphen
(e.g. str.to-int) to underscore (str.to_int)
2019-04-17
Theories/UnicodeStrings.smt2
Draft 2.0
Taking into account some of the feedback from the SMT-LIB community.
In particular, with respect to Draft 1.0 character sort (Char) does not
exists anymore, as this was considered to have more cons than pros.
2018-04-24
Theories/UnicodeStrings.smt2
First draft (Draft 1.0) for the theory of Unicode Strings and Languages
2017-11-24:
Theories/Reals_Ints.smt2:
Added abstract values for irrational numbers to set of Real values,
consistently with the Reals theory (the omission of such values
was an oversight).
2017-07-18:
Standard reference:
Standard reference updated to 2.6
2017-06-13:
Logics/QF_BV.smt2:
Added that bvxor and bvxnor are left associative
Theories/FixedSizeBitVectors.smt2:
Added :left-assoc attribute to bvand, bvor, bvadd, bvmul
2017-05-08:
Theories/Reals.smt2:
Fixed error in note on intepretation of (/t 0).
2017-05-03:
Logics/QF_BV.smt2:
Updated to Version 2.6. Division and remainder operations are no
longer undefiend when the second operand is 0. See
the FixedSizeBitVectors theory definition for details.
Theories/FixedSizeBitVectors.smt2:
Updated to version 2.6; changed semantics of division and
remainder operators.
2016-04-20:
Theories/FixedSizeBitVectors.smt2:
Minor formatting of notes fields.
Theories/Reals.smt2:
Minor formatting of notes fields.
2015-06-28:
Standard reference:
Standard reference minor update (2.5)
2015-05-28:
Standard reference:
Standard reference updated to 2.5
2015-04-25:
Logics/AUFLIA.smt2:
Updated to Version 2.5.
Logics/AUFLIRA.smt2:
Updated to Version 2.5.
Logics/AUFNIRA.smt2:
Updated to Version 2.5.
Logics/LRA.smt2:
Updated to Version 2.5.
Logics/QF_ABV.smt2:
Updated to Version 2.5.
Logics/QF_AUFBV.smt2:
Updated to Version 2.5.
Logics/QF_AUFLIA.smt2:
Updated to Version 2.5.
Logics/QF_AX.smt2:
Updated to Version 2.5.
Logics/QF_BV.smt2:
Updated to Version 2.5.
Logics/QF_IDL.smt2:
Updated to Version 2.5.
Logics/QF_LIA.smt2:
Updated to Version 2.5.
Logics/QF_LRA.smt2:
Updated to Version 2.5.
Logics/QF_NIA.smt2:
Updated to Version 2.5.
Logics/QF_NRA.smt2:
Updated to Version 2.5.
Logics/QF_RDL.smt2:
Updated to Version 2.5.
Logics/QF_UFBV.smt2:
Updated to Version 2.5.
Logics/QF_UFIDL.smt2:
Updated to Version 2.5.
Logics/QF_UFLIA.smt2:
Updated to Version 2.5.
Logics/QF_UFLRA.smt2:
Updated to Version 2.5.
Logics/QF_UFNRA.smt2:
Updated to Version 2.5.
Logics/QF_UF.smt2:
Updated to Version 2.5.
Logics/UFLRA.smt2:
Updated to Version 2.5.
Logics/UFNIA.smt2:
Updated to Version 2.5.
Theories/ArraysEx.smt2:
Updated to Version 2.5.
Theories/Core.smt2:
Updated to Version 2.5.
Theories/FixedSizeBitVectors.smt2:
Updated to Version 2.5.
Theories/FloatingPoint.smt2:
Updated to Version 2.5.
Updated reference to tech report.
Theories/Ints.smt2:
Updated to Version 2.5.
Theories/Reals_Ints.smt2:
Updated to Version 2.5.
Theories/Reals.smt2:
Updated to Version 2.5.
2013-06-24:
Logics/QF_ABV.smt2:
Changed references to Fixed_Size_Bitvectors to FixedSizeBitVectors.
Logics/QF_AUFBV.smt2:
Changed references to Fixed_Size_Bitvectors to FixedSizeBitVectors.
Logics/QF_BV.smt2:
Changed references to Fixed_Size_Bitvectors to FixedSizeBitVectors.
Logics/QF_UFBV.smt2:
Changed references to Fixed_Size_Bitvectors to FixedSizeBitVectors.
Theories/FixedSizeBitVectors.smt2:
Renamed theory's name from Fixed_Size_Bit_Vectors to FixedSizeBitVectors,
for consistency.
Added :value attribute.
2012-09-26:
Logics/AUFNIRA.smt2:
Clarified in :notes in what way AUFNIRA extendes AUFLIRA.
2011-06-15:
Logics/QF_BV.smt2:
Fixed bug in definition of bvsmod. Previously, it gave an incorrect
answer when the divisor is negative and goes into the dividend evenly.
2011-06-03:
Logics/LRA.smt2:
Replaced ''(* c x), or (* x c)'' with ''c, (* c x), or (* x c)''
in :extensions.
(The missing case was had been left out unintentionally.)
Logics/QF_AUFLIA.smt2:
Allowed x to be more than a free constants in terms of the form
(* c x) or (*x c) in :extensions.
Logics/QF_LRA.smt2:
Replaced ''(* c x), or (* x c)'' with ''c, (* c x), or (* x c)''
in :extensions. (The missing case had been left out unintentionally.)
2010-12-16:
Logics/QF_RDL.smt2:
Replaced erroneous ''n > 0'' with ''n > 1'' in language attribute.
2010-08-15:
Theories/ArraysEx.smt2:
Minor fix.
Theories/Core.smt2:
Minor fix.