mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
5449 commits 24 branches 48 tags 158 MiB
Commit graph

712 commits

Author SHA1 Message Date
Nikolaj Bjorner
9253ca9d86 make use of warning_msg safe for formatting. Thanks to Scott McPeak for reporting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-14 08:10:10 -07:00
Nikolaj Bjorner
c7ff05cc78 enable core minimization with qsat in case it turns out to be useful 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-12 15:58:12 -07:00
Christoph M. Wintersteiger
bd187e0989 Bugfix for fp.min/fp.max in fpa2bv converter; hide BV UFs from FP models. 
Fixes #642
 2016-06-09 17:51:31 +01:00
Christoph M. Wintersteiger
879363157f Bugfix for fpa2bv_converter 2016-06-09 12:09:53 +01:00
Nikolaj Bjorner
e9e926d4d6 UINT32_MAX -> UINT_MAX 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-02 21:00:18 -07:00
Nikolaj Bjorner
21158ea03f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-02 20:58:20 -07:00
Nikolaj Bjorner
eab5a84f62 fix issues with int.to.str and seq.len encodings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-02 20:57:52 -07:00
Christoph M. Wintersteiger
83ad5d65e4 Replaced fp.rem conversion to bit-vectors with an SMT-compliant one. 
Fixes #561
 2016-06-02 20:22:02 +01:00
Christoph M. Wintersteiger
ade2dbe15a Cache cleanup fix for bv_simplifier_plugin. 
Fixes #615
 2016-05-31 16:47:14 +01:00
Christoph M. Wintersteiger
03f6b465b9 comment typos 2016-05-31 16:14:50 +01:00
Nikolaj Bjorner
39acd3594a test variants for seq_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-30 18:15:10 -07:00
Nikolaj Bjorner
f03032bd09 updated seq solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-29 14:01:05 -07:00
Nikolaj Bjorner
c3f498a640 strengthen support for int.to.str and length reasoning. Issue #589 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-28 12:26:47 -07:00
Nikolaj Bjorner
18a9b89e30 bypass stale rules as part of unbounded compression. Issue #624 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-27 09:38:23 -07:00
Christoph M. Wintersteiger
15d871cfe0 Bug and style fix for fpa2bv converter. 2016-05-26 13:39:54 +01:00
Nikolaj Bjorner
b8716b3339 avoid use-before-def crashes fp-operations.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-25 14:32:39 -07:00
Christoph M. Wintersteiger
04a68bbb0a Eliminated a number of potential memory leaks in fpa2bv code. 
Relates to #615
 2016-05-25 18:50:57 +01:00
Christoph M. Wintersteiger
617e941015 fp2bv refactoring 2016-05-23 18:10:17 +01:00
Christoph M. Wintersteiger
bf3a5effbc Fixed and refactored fp.min/fp.max for theory_fpa. 
Fixes #616
 2016-05-23 15:38:25 +01:00
Christoph M. Wintersteiger
184aebab59 variable naming 2016-05-23 15:08:27 +01:00
Christoph M. Wintersteiger
d4bc8ebb70 FP to BV translation of UFs refactored. 2016-05-22 18:16:57 +01:00
Christoph M. Wintersteiger
8db17311ae fpa2bv build fixes 2016-05-22 13:13:32 +01:00
Christoph M. Wintersteiger
fe3f8466b6 Partial support for fpa2bv translation in complex types. 2016-05-21 18:08:48 +01:00
Christoph M. Wintersteiger
b6d90a64da fpa rewriter tidy up 2016-05-21 18:07:37 +01:00
Christoph M. Wintersteiger
8001b1f0c7 typo 2016-05-21 17:43:17 +01:00
Christoph M. Wintersteiger
cae53c3ec2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-20 19:55:01 +01:00
Christoph M. Wintersteiger
1cc8146aba Bugfixes for FP UFs and arrays. 2016-05-20 19:53:57 +01:00
Nikolaj Bjorner
1aa3fdab8a remove min/max, use qmax; disable cancellation during model evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-19 13:04:20 -07:00
Christoph M. Wintersteiger
71a03dbeb3 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-18 09:58:11 +01:00
Nikolaj Bjorner
09b8c0e7fa removing warnings for unused variables, #579 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-17 15:59:06 -07:00
Nikolaj Bjorner
96e157e201 fix warnings for unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-17 13:54:22 -07:00
Christoph M. Wintersteiger
df81ab72f5 Bug and performance fixes for FP UFs. 2016-05-17 16:35:45 +01:00
Nikolaj Bjorner
5250c3b9ed ensure reference ownership on frame elements to avoid crashes due to nnf. Issue #588 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-16 09:37:15 -07:00
Nikolaj Bjorner
69ccc02931 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-16 08:35:12 -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
Christoph M. Wintersteiger
44b0a6ddbc Tentative fix for #586. 2016-05-14 18:42:10 +01:00
Christoph M. Wintersteiger
bb2c5972c7 Bugfixes for UFs in theory_fpa. 
Fixes #591, but performance issues remain.
 2016-05-14 18:21:53 +01:00
Nuno Lopes
0286cee450 simplify th_rewriter::mk_eq_value() 2016-05-05 11:00:21 +01:00
Christoph M. Wintersteiger
be424d9cbb Bugfixes for fp.roundToIntegral and fp.rem. 
Relates to #561
 2016-04-24 15:14:16 +01:00
Nikolaj Bjorner
4761f4f191 add handling for int.to.str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-18 11:14:40 -07:00
Christoph M. Wintersteiger
6db0a15d29 Fixed potential memory leakage issues in fpa2bv_converfter 2016-04-18 17:17:31 +01:00
Christoph M. Wintersteiger
3ffcea0fe4 whitespace 2016-04-18 16:52:12 +01:00
Christoph M. Wintersteiger
5971c20653 Bugfixes for bv_trailing. 2016-04-07 13:08:17 +01:00
Nuno Lopes
e2b7ad246a bv_trailing: fix compiler warning + use of ast_manager 2016-04-06 15:34:31 +01:00
Mikolas Janota
dbffc15b98 Improvements in caching of bv_trailing. 2016-04-06 11:04:15 +01:00
mikolas
9ba5bbfd33 Re-factoring and comments in bv_trailing. 2016-04-06 11:04:13 +01:00
Mikolas Janota
248feace34 fixing the behavior in bv_trailing 2016-04-06 11:04:11 +01:00
mikolas
fced47386e More work on trailing 0 analysis. 2016-04-06 11:04:09 +01:00
mikolas
ddb6ae4eab More work on trailing 0 analysis. 2016-04-06 11:04:07 +01:00
mikolas
78cb1e3c7b More work on trailing 0 analysis. 2016-04-06 11:04:05 +01:00