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

7934 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
94d1695b01 Merge branch 'master' of https://github.com/z3prover/z3 2017-12-18 12:20:53 -08:00
Nikolaj Bjorner
399b27fda3 add Python facility for int2bv, fix #1398 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-18 12:20:44 -08:00
Christoph M. Wintersteiger
c3c06d756c Documentation fixes. 2017-12-18 20:12:19 +00:00
Christoph M. Wintersteiger
63951b815d Bumped version number. 2017-12-18 18:58:21 +00:00
Christoph M. Wintersteiger
b0aaa4c6d7 Updated release notes 2017-12-18 14:18:30 +00:00
Nikolaj Bjorner
c3add4eeda add back missing initialization of lo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-15 06:56:36 -08:00
Nikolaj Bjorner
21f685fa5a fix nlsat regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-15 06:54:02 -08:00
Nikolaj Bjorner
397cdfc608 avoid crash on nl 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-15 06:38:56 -08:00
Nikolaj Bjorner
1c3d385c25 fix crashes in nlsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-14 17:24:13 -08:00
Nikolaj Bjorner
ab39f06df7 fix crashes in nlsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-14 17:22:49 -08:00
Nikolaj Bjorner
b28e788371 Merge branch 'master' of https://github.com/z3prover/z3 2017-12-14 17:08:27 -08:00
Nikolaj Bjorner
1dac5bd459 remove comment out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-14 17:07:52 -08:00
Nikolaj Bjorner
e5fa35e969 add integer branch and bound to nlsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-14 17:07:17 -08:00
Christoph M. Wintersteiger
30a02ff45e
Merge pull request #1401 from ivg/fix-ocaml-plugin-build-flags 
fixes compilation flags for OCaml plugins
 2017-12-14 21:52:53 +01:00
Nikolaj Bjorner
58c6cb87c3 small improvements to QF_NIA tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-14 11:48:22 -08:00
Nikolaj Bjorner
387e984bd3 Merge branch 'master' of https://github.com/z3prover/z3 2017-12-13 13:48:34 -08:00
Nikolaj Bjorner
5a479fca76 generalize model finder code to be independent of conjunction elimination 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-13 13:48:24 -08:00
Ivan Gotovchits
49678065bd fixes compilation flags for OCaml plugins 
The `-linkall` option is needed for a plugin to be standalone,
otherwise it will miss those dependencies that are not used.
 2017-12-13 14:45:06 -05:00
Murphy Berzish
d2d79e3207 Merge branch 'master' into develop 2017-12-11 17:36:12 -05:00
Nikolaj Bjorner
82c26509ae
Merge pull request #1396 from mtrberzi/substr-bug 
Fix incorrect term in theory_str str.substr reduction
 2017-12-11 12:36:07 -08:00
Murphy Berzish
83bd103cd4 Merge remote-tracking branch 'upstream/master' into develop 2017-12-11 13:05:04 -05:00
Christoph M. Wintersteiger
2e186633ee Turned assertion failure into proper error message. 2017-12-11 14:59:25 +00:00
Murphy Berzish
9d2c86f214 fix incorrect clause in argumentsValid subterm of substr reduction 2017-12-08 20:31:22 -05: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
c8d9be0bbf fix build of obj_ref_hashtable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-08 14:22:25 +05:30
Nikolaj Bjorner
a5d5dfdf86 fix setup for non-linear real arithmetic per QF_UFNRA regresssions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-08 09:23:57 +05:30
Nikolaj Bjorner
3f19c12a12 add obj_ref_map to make it easier to maintain reference counts with a map of objects 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-08 05:48:34 +05:30
Nikolaj Bjorner
8c8d229ca9 Merge branch 'master' of https://github.com/z3prover/z3 2017-12-07 18:43:53 +05:30
Nikolaj Bjorner
8e1ab23c3d remove deprecated functions from ML API. #1393 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-07 18:43:29 +05:30
Nikolaj Bjorner
0cfea8946b
Merge pull request #1391 from delcypher/cxx_example_use_cxx11 
[CMake] Use C++11 is C++ API example
 2017-12-07 18:38:05 +05:30
Dan Liew
1941a53999 [Release Notes] Note that C++11 is required to build Z3 and is also 
required by the C++ API bindings.
 2017-12-07 10:56:44 +00:00
Dan Liew
92059942e6 [CMake] Use C++11 when building C++ API example. 
This is a change requested by @NikolajBjorner (
5f8c97532c (commitcomment-26049417)
).
 2017-12-07 10:56:44 +00:00
Murphy Berzish
9554723b44 use safer mk_and in extended indexof 2017-12-06 20:50:03 -05:00
Nikolaj Bjorner
39d1ad3edb fix #1390 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-07 05:15:53 +05:30
Nikolaj Bjorner
2770c8f884 disable C++11 dependency to fix the travis build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-05 08:15:23 +05:30
Nikolaj Bjorner
60af4a5820 deal with ambiguity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-04 19:12:51 +05:30
Nikolaj Bjorner
5f8c97532c circumvent build errors introduced when using the ast_vector_tpl iterator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-04 18:10:48 +05:30
Nikolaj Bjorner
fb470a1868 include path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-04 15:32:20 +05:30
Nikolaj Bjorner
a83af22841 include special functionality in parsers for solvers and opt for additional file formats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-03 20:00:45 +01:00
Nikolaj Bjorner
5ee30a3cd9 include special functionality in parsers for solvers and opt for additional file formats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-03 20:00:24 +01:00
Nikolaj Bjorner
187998ae4d
Merge pull request #1381 from NikolajBjorner/smt2 
remove smtlib1 dependencies
 2017-12-02 10:24:02 -08:00
Nikolaj Bjorner
0bfea99cff fix issues found in parsing examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 14:43:52 -08:00
Nikolaj Bjorner
274279b251 Merge branch 'smt2' of https://github.com/nikolajbjorner/z3 into smt2 2017-12-01 09:00:01 -08:00
Nikolaj Bjorner
a9ebda105c remove assertion that gets violated on exception path (declaration of datatypes are not getting removed) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 08:59:36 -08:00
Nikolaj Bjorner
8357210d3c fix lack of warning/error for unbounded objectives in context of quantifiers #1382 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 01:07:41 -08:00
Nikolaj Bjorner
c31ad14747 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 00:52:32 -08:00
Nikolaj Bjorner
4bb0e9b633 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 00:52:06 -08:00
Nikolaj Bjorner
b96dacfff2 set version, fix build of test files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-30 08:42:01 -08:00
Nikolaj Bjorner
c18d60a9c5 fix java 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-29 20:56:36 -08:00
Nikolaj Bjorner
ab58723ffc fix dotnet example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-29 20:52:19 -08:00