mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Code Activity
11480 commits 23 branches 48 tags 156 MiB
Commit graph

11480 commits

This branch
This branch
All branches
Author SHA1 Message Date
Federico Poli 7eb6731ac2 Link pthread with --whole-archive option on Linux 
This fixes a SIGSEGV on Ubuntu 16.04 when running z3 compiled with `--staticbin` (issue #2457). It seems that without the --whole-archive option the linker does not statically link all pthread symbols.

The fix is described here: https://stackoverflow.com/a/45271521/2491528
 2019-11-06 11:18:32 +01:00
Nikolaj Bjorner a78f899225 expand deep stores by lambdas to avoid expanding select/store axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-03 10:29:10 +01:00
Nikolaj Bjorner d866a93627 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-03 10:29:10 +01:00
Samuel Thibault da061bbcc3 Add hurd support 
Signed-off-by: Samuel Thibault <samuel.thibault@ens-lyon.org>
 2019-11-03 01:22:44 -08:00
Nikolaj Bjorner 16d4ccd396 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-31 10:06:09 -07:00
Nikolaj Bjorner 18b8089a1e Revert "remove unused random seed parameter on cmd_context" 
This reverts commit e2a9cb80e2.
 2019-10-29 11:05:50 -07:00
Christoph M. Wintersteiger 4faaff5b76
Fix memory leak in bv2fpa_converter 2019-10-28 14:15:30 +00:00
Christoph M. Wintersteiger 2308d8af09
Fix for partially interpreted floating-point functions. Relates to #2596, #2631. 2019-10-28 14:15:29 +00:00
Christoph M. Wintersteiger 1d4f8c0168
Typos 2019-10-28 14:15:29 +00:00
Christoph M. Wintersteiger efa3c0f68e
Fix compiler warnings 2019-10-28 14:15:25 +00:00
Nikolaj Bjorner 823bf317c5 fix #2664 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-28 05:11:46 -07:00
Nikolaj Bjorner d0dac83143 fix #2665 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-28 04:59:18 -07:00
Nikolaj Bjorner e24481dacd fix #2662 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-28 04:38:57 -07:00
Nikolaj Bjorner 376d2c1ed4 add unit test based on #2658 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-25 18:07:43 -07:00
Murphy Berzish be99d3d450 z3str3: refactoring, move regex automata methods to theory_str_regex 2019-10-25 18:06:06 -07:00
philzook58 ed03c1d9e6 Removed incorrect include directories flag in ocaml META file 2019-10-25 18:05:13 -07:00
Nikolaj Bjorner 14c42c1d74 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-25 10:42:21 -07:00
Nikolaj Bjorner 64dd4e1c83 fix #2659 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-25 10:42:21 -07:00
Nikolaj Bjorner a8049c7feb update nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-24 16:34:41 -07:00
Murphy Berzish b9a407c25f z3str3: force eager axiom setup on new terms 2019-10-24 15:20:07 -07:00
Murphy Berzish f91af02675 z3str3: set up axioms on string terms that are added during the search 2019-10-24 15:20:07 -07:00
Michał Janiszewski 9ae1a6f061 Add MSVC ARM64 job to Azure Pipelines 2019-10-24 15:19:53 -07:00
Michał Janiszewski 3feb1479c9 Improve platform detection, in particular MSVC ARM64 2019-10-24 15:19:53 -07:00
Michał Janiszewski 907ffde577 Drop explicit MSVC's DYNAMICBASE option setting in favour of defaults 
This option is not supported on Arm64 and the defaults should be fine
 2019-10-24 15:19:53 -07:00
Michał Janiszewski 837651e318 Explicitly add EHsc to MSVC compiler flags 2019-10-24 15:19:53 -07:00
Nikolaj Bjorner 60dde9f3d5 unit test for #2650 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-24 10:32:56 -07:00
Nikolaj Bjorner 8125fb134f na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-23 20:19:06 -07:00
Nikolaj Bjorner 3fcd9e64c7 logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-23 20:18:21 -07:00
Nikolaj Bjorner f4fd94747c fix #2652 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-23 09:39:40 -07:00
Nikolaj Bjorner e2a9cb80e2 remove unused random seed parameter on cmd_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-22 08:42:18 -07:00
Nikolaj Bjorner 9847675095 fix #2647 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-22 08:26:40 -07:00
Murphy Berzish 76b3198282 z3str3: fixes to str.indexof when axiomatizing constant expressions 2019-10-22 07:53:14 -07:00
Nikolaj Bjorner 0acbdffacf update mk_nuget_task 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 15:34:05 -07:00
Nikolaj Bjorner bfc30440ac update nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 13:57:45 -07:00
Nikolaj Bjorner 9fae4a16e6 update nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 12:35:12 -07:00
Nikolaj Bjorner 4051fbd8b2 update nuget packaging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 11:19:28 -07:00
Nikolaj Bjorner f086f01ae0 update nuget script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 10:09:37 -07:00
Nikolaj Bjorner 928e08f28f update nightly runner 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 09:31:28 -07:00
Nikolaj Bjorner af442cf281 update nightly runner 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 09:29:43 -07:00
Nikolaj Bjorner 0756581a99 add nuget stage to nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 08:22:18 -07:00
Nikolaj Bjorner 5c78f855ad re-add deletion for nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 07:49:57 -07:00
Nikolaj Bjorner aef0c19d36 add pdb to distribution components 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-21 07:48:45 -07:00
Nikolaj Bjorner e5504247e9 use propagation filter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-20 16:00:20 -07:00
Nuno Lopes 423e084cda remove unused var 2019-10-19 17:36:57 +01:00
Nikolaj Bjorner 11736f078e ensure statistics survive cancelation in tactics, fix propagation for smtfd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-18 19:22:46 -07:00
Nikolaj Bjorner 203ba12abc moving to context reset model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-18 19:22:46 -07:00
Nikolaj Bjorner 724a42b6f2 fix #2643 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-18 09:48:55 -07:00
philzook58 5eead52cc0 Fixed linkopts -lstdc++ for ocaml bindings 2019-10-17 10:52:38 -07:00
Nikolaj Bjorner c1fa844460 format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-17 10:01:11 -07:00
Nikolaj Bjorner a82cee6984 add information about supported packages in README, fix #2642 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-17 10:00:41 -07:00