Arie Gurfinkel
|
2ec00cb81d
|
Replace is_null with is_non_empty_string in spacer params
|
2020-03-31 11:21:05 -04:00 |
|
Arie Gurfinkel
|
cfe96fe92e
|
[spacer] fixedpoint.get_answer() returns ground refutation for SAT
|
2020-03-31 10:13:37 -04:00 |
|
Nuno Lopes
|
79eb6a0e66
|
reduce_invertible: fix mk_diagonal for BV 0
switch from -x to ~x
|
2020-03-31 12:22:43 +01:00 |
|
Nuno Lopes
|
0b6b267ec4
|
minor code simplification in bv rewriter
|
2020-03-31 11:04:04 +01:00 |
|
Nuno Lopes
|
91497f923a
|
reduce_invertible: recognize (* x -1) as the same as (- x)
|
2020-03-31 10:54:03 +01:00 |
|
Lev Nachmanson
|
cf0952c232
|
roll back in maximize_term if the integrality is broken
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-30 17:59:45 -07:00 |
|
Nikolaj Bjorner
|
f21b60a6e1
|
remove output from normalize bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 17:46:53 -07:00 |
|
Nikolaj Bjorner
|
e2cab00b1b
|
fix #3583
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 17:37:57 -07:00 |
|
Nikolaj Bjorner
|
48581eb7ab
|
fix #3598, feature overload abuse
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 17:29:02 -07:00 |
|
Nikolaj Bjorner
|
296e56c28f
|
fix #3575
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 17:26:43 -07:00 |
|
Nikolaj Bjorner
|
03d7a9acff
|
#3581, bail out when smt solver gives up
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 17:19:57 -07:00 |
|
Nikolaj Bjorner
|
330b3cc8d6
|
fix #3584
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 16:50:53 -07:00 |
|
Nikolaj Bjorner
|
7f8738dd85
|
fix #3542
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 16:24:47 -07:00 |
|
Lev Nachmanson
|
3e845010dd
|
replace v by j in lp printouts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-30 15:59:03 -07:00 |
|
Nikolaj Bjorner
|
a6e7ed039c
|
fix #3587
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 15:18:37 -07:00 |
|
Nikolaj Bjorner
|
8a961a5ce9
|
fix #3554
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 15:02:55 -07:00 |
|
Nikolaj Bjorner
|
0ca5f59e35
|
fix #3550
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 14:45:38 -07:00 |
|
Nikolaj Bjorner
|
fe81de6d39
|
fix #3555
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 14:37:38 -07:00 |
|
Nikolaj Bjorner
|
b9dd18483c
|
fix #3571
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 14:11:36 -07:00 |
|
Nikolaj Bjorner
|
d4aa850412
|
fix #3572
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 14:09:47 -07:00 |
|
Nikolaj Bjorner
|
e263f9b238
|
fix #3559
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 14:00:30 -07:00 |
|
Nikolaj Bjorner
|
de2ad26826
|
fix #3568
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 13:51:45 -07:00 |
|
Nikolaj Bjorner
|
04e51ffcb5
|
fix #3569
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 13:40:59 -07:00 |
|
Nikolaj Bjorner
|
53b5ca3c2b
|
disambiguate call
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 13:35:40 -07:00 |
|
Nikolaj Bjorner
|
5152c9500d
|
fix #3591
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 13:08:58 -07:00 |
|
Nikolaj Bjorner
|
bf9779cb87
|
fix #3593
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 12:46:18 -07:00 |
|
Nikolaj Bjorner
|
aeee44398d
|
fix #3594
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 12:40:24 -07:00 |
|
Lev Nachmanson
|
7936df8e0b
|
pass std::function as const aliases
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-30 12:20:47 -07:00 |
|
Nikolaj Bjorner
|
ba4765f16f
|
debugging #3511
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 11:00:02 -07:00 |
|
Nikolaj Bjorner
|
f74079de01
|
fix #3529
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 11:00:02 -07:00 |
|
Nikolaj Bjorner
|
c142f99127
|
fix #3532
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 11:00:02 -07:00 |
|
Nikolaj Bjorner
|
0b10cb3312
|
fix #3528
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 11:00:02 -07:00 |
|
Lev Nachmanson
|
9be7bda69a
|
fix a bug in column patching
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-29 15:03:46 -07:00 |
|
Lev Nachmanson
|
7a950dd667
|
patch reals
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-29 15:03:46 -07:00 |
|
Lev Nachmanson
|
3237bd9243
|
better tracing
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-29 15:03:46 -07:00 |
|
Nikolaj Bjorner
|
7086a7c26a
|
fix #3531
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-29 11:15:01 -07:00 |
|
Nikolaj Bjorner
|
1155db383e
|
fix #3540
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-29 10:55:47 -07:00 |
|
Nikolaj Bjorner
|
9f386306ef
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-29 10:55:47 -07:00 |
|
Nikolaj Bjorner
|
1a995da0ae
|
fix #3538, turn on proof checking assertions in goal.cpp for earlier coverage
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-29 10:55:47 -07:00 |
|
Lev Nachmanson
|
907d310600
|
get rid of arith.nla parameter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-27 14:33:40 -07:00 |
|
Lev Nachmanson
|
f9151a7a8e
|
correct the default options: smt.arith.nla=False
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-27 13:55:23 -07:00 |
|
Nikolaj Bjorner
|
4b7bd3a881
|
fix #3536
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-27 12:59:24 -07:00 |
|
Nikolaj Bjorner
|
f8dcaa8885
|
'na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-27 10:23:00 -07:00 |
|
Lev Nachmanson
|
352f4b5b37
|
use u_set in random_update()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-03-26 18:11:32 -07:00 |
|
Nikolaj Bjorner
|
12f62e73d5
|
fix ordering of delayed assume eqs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 16:24:34 -07:00 |
|
Nikolaj Bjorner
|
7a04e52c41
|
fix ordering of delayed assume eqs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 16:22:24 -07:00 |
|
Nikolaj Bjorner
|
499843ae7f
|
remove verbose 0 output, #3527
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 14:49:14 -07:00 |
|
Arie Gurfinkel
|
5673ec046b
|
qe_term_graph fix for #3526
|
2020-03-26 16:45:06 -04:00 |
|
Nikolaj Bjorner
|
d4699b181d
|
fix assertion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 12:49:44 -07:00 |
|
Nikolaj Bjorner
|
73ab95d338
|
remove canonize in seq solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 12:47:30 -07:00 |
|