Nikolaj Bjorner
|
640cf1809d
|
Merge pull request #4585 from iscottb122/dotnet_fp_significand
Return significand bits correctly (dotnet API). Fixes #4584
|
2020-07-22 09:59:30 -07:00 |
|
Iain Scott
|
b6867d69c2
|
Return significand bits correctly (dotnet API). Fixes #4584
|
2020-07-22 16:57:33 +01:00 |
|
Nikolaj Bjorner
|
ed58175e1b
|
issue #4582
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-21 18:23:41 -07:00 |
|
Nikolaj Bjorner
|
aab50ff3f5
|
fixing bugs reported in #4518
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-21 15:50:19 -07:00 |
|
Nikolaj Bjorner
|
b1824fea10
|
fix lifetimes for crashes in #4525
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-21 12:53:56 -07:00 |
|
Nikolaj Bjorner
|
f17ead21f9
|
fix #4578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-21 10:11:39 -07:00 |
|
Nikolaj Bjorner
|
1d8d85add9
|
fix #4575 - correction set resolution only works with uniform weights
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-20 15:05:06 -07:00 |
|
Nikolaj Bjorner
|
ebce0b3612
|
fix #4577
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-20 14:40:45 -07:00 |
|
Nikolaj Bjorner
|
61b85d7123
|
verbosity
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-20 14:11:59 -07:00 |
|
Nikolaj Bjorner
|
e8b5abe63e
|
revert - copy over xml in mk-dist mode #4578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-20 11:17:29 -07:00 |
|
Nikolaj Bjorner
|
a7b71239ae
|
copy over xml in mk-dist mode #4578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-20 10:22:57 -07:00 |
|
Nikolaj Bjorner
|
00491148f0
|
string
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-20 10:22:57 -07:00 |
|
Nikolaj Bjorner
|
549ef0e052
|
fix typos #4573
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-20 10:22:57 -07:00 |
|
Christoph M. Wintersteiger
|
a298091322
|
Fix for fp.roundToIntegral of tiny, denormal floats. Fixes #4190.
|
2020-07-17 15:58:01 +00:00 |
|
Christoph M. Wintersteiger
|
2ef57d7f8d
|
Fix FP rounding of huge exponents. Fixes #3776.
|
2020-07-17 13:42:12 +00:00 |
|
Christoph M. Wintersteiger
|
d3ae40130a
|
Fix rounding bug in mpf_manager. Fixes #2970.
|
2020-07-16 12:39:12 +00:00 |
|
Christoph M. Wintersteiger
|
ccdae7af24
|
Fix for corner-case in fp.roundToIntegral. Fixes #2894.
|
2020-07-16 11:58:18 +00:00 |
|
Christoph M. Wintersteiger
|
c321fb7726
|
Correctly report unsupported features in bvarray2uf_rewriter. Fixes #4046 and #4047.
|
2020-07-15 16:16:29 +00:00 |
|
Christoph M. Wintersteiger
|
7dd28708a1
|
Fix bug in qprofdiff. Fixes #4521.
|
2020-07-15 15:13:11 +00:00 |
|
Nuno Lopes
|
b7caabbd0f
|
fix crashes with MSVC 2019
|
2020-07-14 13:14:44 +01:00 |
|
Nuno Lopes
|
aeac0b46a0
|
remove copy
|
2020-07-14 12:26:49 +01:00 |
|
Nuno Lopes
|
d1a0e83423
|
fix crash
|
2020-07-13 14:25:12 +01:00 |
|
Nuno Lopes
|
122f5a1464
|
remove unused field
|
2020-07-12 23:12:00 +01:00 |
|
Nuno Lopes
|
90fc8d854f
|
add rval methods to scoped_vector
|
2020-07-12 22:16:24 +01:00 |
|
Nuno Lopes
|
f30e8ccec3
|
fix crashes due to my last commit
|
2020-07-12 19:53:22 +01:00 |
|
Nuno Lopes
|
bb26f219fe
|
remove unneeded constructors (last round)
|
2020-07-12 17:41:57 +01:00 |
|
Nuno Lopes
|
44ec259c4c
|
fix python test
|
2020-07-11 22:33:47 +01:00 |
|
Nuno Lopes
|
23e6adcad3
|
fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string
|
2020-07-11 20:24:45 +01:00 |
|
Nikolaj Bjorner
|
48a9defb0d
|
fix #1484 'regression'
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-09 15:09:25 -07:00 |
|
Nikolaj Bjorner
|
6b380811b8
|
fix #4524
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-09 15:05:55 -07:00 |
|
Nikolaj Bjorner
|
65e6b73873
|
fix #4538 - regression when renaming family from special_relations to specrels
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-08 14:46:40 -07:00 |
|
Nikolaj Bjorner
|
80cc45c5c1
|
display justifications compactly for tracing #4575
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-08 13:32:41 -07:00 |
|
Nikolaj Bjorner
|
ab7b8b6ec5
|
fix #4572
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-08 11:58:44 -07:00 |
|
Nikolaj Bjorner
|
061abd153c
|
fixing #4515
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-08 11:43:32 -07:00 |
|
Nikolaj Bjorner
|
ec3066c28a
|
#4532 - arithmetic using SAT for interpreted atoms such as (< 0 0)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-08 11:43:32 -07:00 |
|
Nikolaj Bjorner
|
e1a0a2e536
|
give up on addition subterms in monomial decomposition caused by disabling rewriter.flat seems to be corner case exercised in #4532.
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-08 11:43:32 -07:00 |
|
Nikolaj Bjorner
|
69afd9f6bd
|
formatting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-08 11:43:31 -07:00 |
|
Nikolaj Bjorner
|
9bcda408ba
|
towards closing small domain equality enforcement gap #4515
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-08 11:43:31 -07:00 |
|
Christoph M. Wintersteiger
|
3776588375
|
Clarify bit-blasting of fp.neg. Fixes #4466.
|
2020-07-08 18:24:08 +00:00 |
|
Christoph M. Wintersteiger
|
c59519bf9c
|
Add missing FP conversion. Fixes #4470.
|
2020-07-08 17:56:25 +00:00 |
|
Nikolaj Bjorner
|
688d38d868
|
typo
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-07 19:07:26 -07:00 |
|
Nikolaj Bjorner
|
4e77984c57
|
enable binary string access to unsigned numerals over API #4568
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-07 18:59:20 -07:00 |
|
Nikolaj Bjorner
|
4b346ef693
|
enable binary string access to unsigned numerals over API #4568
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-07 18:58:42 -07:00 |
|
Nikolaj Bjorner
|
4a8533e41f
|
enable binary string access to unsigned numerals over API #4568
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-07 18:17:54 -07:00 |
|
Nikolaj Bjorner
|
2d358a9a50
|
fix #4565
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-06 17:07:37 -07:00 |
|
Nuno Lopes
|
ca97bfb4b8
|
fix build
|
2020-07-05 11:44:12 +01:00 |
|
Nikolaj Bjorner
|
006418e027
|
build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-04 23:34:21 -07:00 |
|
Nikolaj Bjorner
|
f380d4cf83
|
mpfx
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-04 18:25:32 -07:00 |
|
Nikolaj Bjorner
|
74eb401c3b
|
addrecdef
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-04 18:18:25 -07:00 |
|
Nikolaj Bjorner
|
51d43c04ea
|
st
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-04 17:13:04 -07:00 |
|