Nikolaj Bjorner
|
00a4f6ad3d
|
throw
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-26 15:28:38 -07:00 |
|
Nikolaj Bjorner
|
1d223b0403
|
setting ctx to null after close
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-26 14:59:19 -07:00 |
|
Nikolaj Bjorner
|
2eea7709e0
|
Merge pull request #2438 from agurfinkel/issue_2430
Fix issue 2430
|
2019-07-26 08:18:29 -07:00 |
|
Nikolaj Bjorner
|
53aded3198
|
fix #2416 exposed bugs: unsat-core extraction in combination with chronological backracking, equivalence elimination in combination with PB constraints
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-25 18:55:44 -07:00 |
|
Arie Gurfinkel
|
92db639caf
|
Use refutation to compute ground sat answer
|
2019-07-25 15:22:37 -04:00 |
|
Nikolaj Bjorner
|
8a0d79251e
|
make sorting of soft constraints the same across implementations of std::sort
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-25 11:32:49 -07:00 |
|
Nikolaj Bjorner
|
e6df7b73aa
|
fix #2434
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-25 09:40:18 -07:00 |
|
Nikolaj Bjorner
|
ca25e482e5
|
temporarily disable elim_pure
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-24 19:01:23 -07:00 |
|
Nikolaj Bjorner
|
c75a57731f
|
fix #2433
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-24 14:14:18 -07:00 |
|
Nikolaj Bjorner
|
859512d937
|
fix #2431
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-24 12:14:02 -07:00 |
|
Nikolaj Bjorner
|
e17b43617c
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-24 12:05:48 -07:00 |
|
Nikolaj Bjorner
|
604e6b2705
|
fix #2418, change types in sat_solver to avoid cast
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-24 11:52:28 -07:00 |
|
Nikolaj Bjorner
|
809b0ebca7
|
revert fix to #2417
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-24 11:24:01 -07:00 |
|
Nikolaj Bjorner
|
3a90de1cbe
|
fix #2419
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-24 10:09:34 -07:00 |
|
Nikolaj Bjorner
|
e65a5d0f47
|
fix #2420
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-24 09:56:11 -07:00 |
|
Nikolaj Bjorner
|
019d78e219
|
fix #2422
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-24 09:51:04 -07:00 |
|
Nikolaj Bjorner
|
1a70fce92e
|
add back nvars
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-24 09:51:04 -07:00 |
|
Nikolaj Bjorner
|
185b01dd35
|
fix #2416
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-23 19:01:49 -07:00 |
|
Nikolaj Bjorner
|
c2264c73f2
|
debug mutex
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-23 19:01:49 -07:00 |
|
Nikolaj Bjorner
|
df04d7f108
|
Merge pull request #2428 from danielschemmel/warnings
Fix Some Warnings
|
2019-07-23 08:45:34 -07:00 |
|
Daniel Schemmel
|
77d5b381ea
|
Order initialization to avoid -Wreorder
|
2019-07-23 11:12:29 +02:00 |
|
Daniel Schemmel
|
5e5c231712
|
Remove unused variables
|
2019-07-23 11:09:50 +02:00 |
|
Nikolaj Bjorner
|
364fbda925
|
expose reorder config
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-22 15:30:06 -07:00 |
|
Nikolaj Bjorner
|
aff4b3022a
|
fix #2417
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-21 10:57:52 -07:00 |
|
Nikolaj Bjorner
|
a9a26e5f2e
|
review comments by Elffers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-21 06:52:02 -07:00 |
|
Nikolaj Bjorner
|
e593b5b2c8
|
fix #2415
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-20 16:23:01 -07:00 |
|
Nikolaj Bjorner
|
43a19cadf6
|
avoid reorder regression. affects performance of SAT and also noticably for #2405
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-20 12:40:22 -07:00 |
|
Nikolaj Bjorner
|
41ca956012
|
expose import model converter over Python, document it, add partial order axioms for lex, disable linear order axioms, prepare ground for re-adding clauses from reconstruction stack
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-18 13:45:13 -07:00 |
|
Nikolaj Bjorner
|
7ed5ca05e3
|
fix #2408
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-18 08:37:00 -07:00 |
|
Nikolaj Bjorner
|
d07f2d45e7
|
fix #2409
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-18 08:33:58 -07:00 |
|
Nikolaj Bjorner
|
1fca76b0a1
|
relax restriction on infinitesimal for rdl, #2410
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-18 08:26:23 -07:00 |
|
Nikolaj Bjorner
|
5820b16800
|
mark assumption literals to be skolem to hide them from models #2406
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-18 08:25:42 -07:00 |
|
Nikolaj Bjorner
|
4b6a7371dd
|
insert fresh
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-18 06:31:47 -07:00 |
|
Nikolaj Bjorner
|
fb124d6e93
|
Merge pull request #2393 from Nils-Becker/master
Fix Incorrect Logging of Newly Introduced Terms During Rewrite
|
2019-07-14 09:25:06 -04:00 |
|
Nikolaj Bjorner
|
4deb9d2af2
|
use array interpretations whenever possible for #2378. Also strengthen equality test for lambda
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-14 09:23:29 -04:00 |
|
Nikolaj Bjorner
|
3ca32efd18
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-13 16:22:09 -04:00 |
|
Nikolaj Bjorner
|
2d4e9a0f67
|
update managed APIs for lambda-based array models #2400
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-13 16:20:36 -04:00 |
|
Nikolaj Bjorner
|
659be6940b
|
fix #2395
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-12 18:01:26 -04:00 |
|
Nikolaj Bjorner
|
26c1c744aa
|
fix #2396
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-12 17:36:30 -04:00 |
|
Nikolaj Bjorner
|
0bca2aabff
|
remove invocation of debugger
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-12 17:07:44 -04:00 |
|
Nikolaj Bjorner
|
559af09b07
|
fix index cases
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-12 19:01:39 +01:00 |
|
Nikolaj Bjorner
|
84990ffa27
|
fixing #2378
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-12 14:21:22 +01:00 |
|
Nikolaj Bjorner
|
be72accaf5
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-12 12:37:46 +01:00 |
|
Nikolaj Bjorner
|
1538b31dd9
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-12 12:37:24 +01:00 |
|
Nikolaj Bjorner
|
d861b91289
|
augment axiomatization for substr to fix #2366
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-12 11:13:05 +01:00 |
|
Nikolaj Bjorner
|
79e4b84507
|
augment axiomatization for substr to fix #2366
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-12 11:12:01 +01:00 |
|
Nikolaj Bjorner
|
1ba6d16c61
|
augment axiomatization for substr to fix #2366
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-12 08:38:33 +01:00 |
|
nilsbecker
|
308647efd9
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2019-07-11 17:22:10 +02:00 |
|
nilsbecker
|
335072eda2
|
extract logging into separate function
|
2019-07-11 17:22:03 +02:00 |
|
Nikolaj Bjorner
|
cfb4d289b8
|
fix #2325
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-11 10:34:35 +01:00 |
|