mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
8123 commits 49 branches 53 tags 182 MiB
Commit graph

8123 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
041520f727 SMT2 compliancy fix; NRA includes conversion of Int numerals 2017-03-28 18:17:22 +01:00
Nikolaj Bjorner
0c4b792dac Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-25 19:32:17 +01:00
Nikolaj Bjorner
3a9857940e add missing axioms for str.at. Issue #953 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-25 19:31:01 +01:00
Nikolaj Bjorner
723b507a88 properly handle recursive function definitions #898 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-24 10:11:39 -07:00
Nikolaj Bjorner
e05cee757b properly handle recursive function definitions #898 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-24 10:10:42 -07:00
Christoph M. Wintersteiger
3bbe5eceeb fix for --get-describe 2017-03-24 15:53:46 +00:00
Christoph M. Wintersteiger
f8d022a180 Non-windows build fix 2017-03-24 15:25:18 +00:00
Christoph M. Wintersteiger
fb105afac2 Windows build fix 2017-03-24 15:22:33 +00:00
Christoph M. Wintersteiger
0399e5e2d3 Fixed variable initialization warning 2017-03-24 14:49:24 +00:00
Christoph M. Wintersteiger
d10dec2218 Removed unused variable 2017-03-24 14:31:06 +00:00
Christoph M. Wintersteiger
7f9c37e19d VS2017 SSE4 intrinsics build fix 2017-03-24 14:23:39 +00:00
Christoph M. Wintersteiger
e9cd4d1057 Build fix for systems that don't come with SSE4.1 support by default 2017-03-24 11:51:36 +00:00
Christoph M. Wintersteiger
46ff4ae40d Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-24 09:40:23 +00:00
Christoph M. Wintersteiger
866035d786 Disabled debug output 2017-03-24 09:40:18 +00:00
Nikolaj Bjorner
ec47706226 fix constant offset and handling of ite in difference logic optimizer code-path. Issue #946 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-24 02:23:50 -07:00
Nikolaj Bjorner
5d11a1cdb2 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-24 01:31:16 -07:00
Nikolaj Bjorner
c56c7fd649 add handlers for dense difference logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-24 01:31:00 -07:00
Christoph M. Wintersteiger
37167a8dd6 Fixed excessive trace output 2017-03-23 19:53:23 +00:00
Nikolaj Bjorner
0313f52cf2 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-23 11:10:32 -07:00
Nikolaj Bjorner
62e87d6474 fix double ownership of enode marking causing crash during tracing. Issue #952 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-23 11:10:19 -07:00
Nikolaj Bjorner
1ab7ab9d74 fix double ownership of enode marking causing crash during tracing. Issue #952 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-23 11:09:36 -07:00
Murphy Berzish
82d472a227 Merge remote-tracking branch 'upstream/master' into develop 2017-03-23 13:35:58 -04:00
Nikolaj Bjorner
26ae3a5abb making simplifier code exception friendlier. Towards getting a handle on #939 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-22 19:06:59 -07:00
Nikolaj Bjorner
e47e8c67c0 introducing scoped detacth/attach of clauses to enforce basic sat solver invariants. Part of investigating #939: 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-22 14:12:47 -07:00
Nikolaj Bjorner
25d839ed10 fix bug in simplifier of bv2int over concatentations exposed by #948 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-22 10:55:55 -07:00
Nikolaj Bjorner
e342b87921 Merge pull request #942 from mtrberzi/str-extract-semantics 
alternate str.extract semantics in seq_rewriter
 2017-03-21 10:48:06 -07:00
Murphy Berzish
6804c88b66 make seq.extract rewrite type-generic 2017-03-21 12:54:06 -04:00
Nikolaj Bjorner
6be4c9a5bb Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-21 07:40:40 -06:00
Nikolaj Bjorner
ca4ae171ea remove unsound simplification in prefix #949 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-21 07:40:35 -06:00
Nuno Lopes
8ac060c549 fix build with VS 2017 2017-03-20 09:12:41 +00:00
Nikolaj Bjorner
d58018841e remove code that causes infinite loop. Stackoverflow question from Dominik Wojtaszek 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-17 10:52:16 -07:00
Murphy Berzish
43f9a0a2bd fix unterminated char* 2017-03-17 13:48:30 -04:00
Nikolaj Bjorner
d754aa2dc4 disable ackerman reduction when head contains a non-constant/non-variable. #947 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-17 10:12:32 -07:00
Nikolaj Bjorner
a0237ed2a6 fix crash reported in #946 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-16 18:56:43 -07:00
Murphy Berzish
8021d63539 remove legacy str_decl_plugin and str_rewriter classes; these have been unified with sequence-compatible equivalents 2017-03-15 15:25:48 -04:00
Nikolaj Bjorner
72651e2e98 fixing sources for double frees of clauses. #940 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-14 19:35:11 -07:00
Nikolaj Bjorner
05c267b8d8 make seq.at operations generic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-14 15:37:47 -07:00
Murphy Berzish
5917a34226 Merge branch 'upstream-master' into develop 2017-03-14 15:04:17 -04:00
Murphy Berzish
9659f08322 Merge branch 'str-extract-semantics' into develop 2017-03-14 14:14:53 -04:00
Murphy Berzish
34717a7b6e str.extract semantics fix 2017-03-14 14:14:46 -04:00
Nikolaj Bjorner
0668ba5f6c add pb shorthands to C++. Issue #694 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-14 07:58:39 -07:00
Nikolaj Bjorner
7634f8b93e Merge branch 'master' of https://github.com/Z3Prover/z3 2017-03-14 07:47:51 -07:00
Nikolaj Bjorner
1dd2de61ec add sum shorthand to C++. Issue #694 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-03-14 07:43:26 -07:00
Nikolaj Bjorner
dc9266f95a Merge pull request #941 from humeafo/master 
added no exception support to z3++.h
 2017-03-14 15:37:26 +01:00
hume
0b1d564509 added no exception support to z3++.h 2017-03-14 18:11:00 +08:00
Murphy Berzish
24df976f95 fixup startswith/endswith to prefixof/suffixof 2017-03-13 17:03:36 -04:00
Nikolaj Bjorner
5cff42bbfa Merge pull request #938 from mtrberzi/str-at-semantics 
alternate str.at semantics check in seq_rewriter
 2017-03-13 19:50:02 +01:00
Murphy Berzish
94d5f242b8 Merge branch 'str-at-semantics' into develop 2017-03-13 14:40:40 -04:00
Murphy Berzish
5c9d7538a0 add alternate str.at semantics check in seq_rewriter 
this rewrites to empty string if the index is negative or beyond the length of the string,
which is consistent with CVC4's semantics for this term
 2017-03-13 14:39:12 -04:00
Nikolaj Bjorner
5a79722071 Merge pull request #926 from delcypher/cmake_z3_config 
[CMake] Z3 Package config files
 2017-03-13 15:17:38 +01:00