3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-16 09:26:39 +00:00
Commit graph

19 commits

Author SHA1 Message Date
Nuno Lopes
cef17c22a1 remove some allocs from exceptions 2018-07-02 17:08:02 +01:00
Nikolaj Bjorner
19e2f8c9d5 fix #1694
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-20 17:35:41 -07:00
Nikolaj Bjorner
8040eddf65 fix #1658 fix #1689
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-18 16:41:04 -07:00
Nikolaj Bjorner
c513f3ca09 merge with master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-25 14:57:01 -07:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Bruce Mitchener
7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07:00
Nikolaj Bjorner
79a9dfd8fd adding pre-processing to nlsat for equations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-12-30 20:35:33 -08:00
Nikolaj Bjorner
faebbc5384 add shortcuts for concatenation and equality propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-12-08 16:17:04 +05:30
Nikolaj Bjorner
2f218b0bdc remove also cores as arguments to tactics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-19 12:18:50 -08:00
Nikolaj Bjorner
4bbece6616 re-organize proof and model converters to be associated with goals instead of external
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-18 16:33:54 -08:00
Nikolaj Bjorner
df6b1a707e remove proof_converter from tactic application, removing nlsat_tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-17 23:32:29 -08:00
Nikolaj Bjorner
2ede4b2c80 fixes based on regression tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-27 09:31:16 -07:00
Nikolaj Bjorner
f99048f3e7 rewrite to address some cases like #1203, updates to division handling in NRA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-12 13:24:54 -07:00
Nikolaj Bjorner
7b47b0380e update Ackerman reduction for division to make Andre and Nathan happy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-10 23:43:21 +02:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 13:24:11 -07:00
Nikolaj Bjorner
f1b63691d8 Fixing issue #605 rlimit responsiveness in mam
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-05-16 08:35:04 -07:00
Nikolaj Bjorner
1a5449c3d4 enable new NRA solver for nra benchmarks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-20 12:35:29 -07:00
Nikolaj Bjorner
92b5aac12a adjusting new tactics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-20 10:13:23 -07:00
Nikolaj Bjorner
20bbdfe31a moving remaining qsat functionality over
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-19 15:35:26 -07:00