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

9402 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 0d4b4b30b1 change storage layout of .Net binding Z3_bool to byte to deal with uninitialized memory reads on larger allocation sizes. Bug introduced when switching from defining Z3_bool as int to the bool type from stdbool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 02:58:06 -07:00
Nikolaj Bjorner b38abf64d7 use expr_ref on mk_concat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 19:30:46 -07:00
Nikolaj Bjorner 13413d0529 update for int return value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 15:08:16 -07:00
Nikolaj Bjorner fad1e611aa build warnings, updates to reduce-invertible, change is_algebraic tester to use int return type 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 12:34:55 -07:00
Nikolaj Bjorner b8b70c53fa update invertible tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 09:17:20 -07:00
Nikolaj Bjorner e027622886 updates to invertible tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-30 21:46:29 -07:00
Nikolaj Bjorner 76417fa3b6 fleshing out reduce-invertible tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-30 17:06:56 -07:00
Nikolaj Bjorner ac014bef94 outline of invertible reduction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-30 13:46:29 -07:00
Nikolaj Bjorner cce3448fd5 workaround for heisenbug behavior with tester 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-30 11:56:01 -07:00
Nikolaj Bjorner c4d893dfad fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-30 06:10:09 -07:00
Nikolaj Bjorner 080bf79fe6
Merge pull request #1705 from trinhmt/master 
created pull from Trinh's seq solver
 2018-06-30 04:53:14 -07:00
Thai Trinh cd62017afd fixed failures with regression tests 2018-06-30 15:52:20 +08:00
Nikolaj Bjorner 3ad7d59f22 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-29 21:25:21 -07:00
Nikolaj Bjorner 797e576195 unreferenced variable in release mode, spaces 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 21:25:08 -07:00
Nikolaj Bjorner 33fc56f686 fix debug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 18:36:43 -07:00
Nikolaj Bjorner f1d27cd487 workaround non-deterministic behavior of is_irrational_numeral test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 18:16:32 -07:00
Nikolaj Bjorner 481b177d47 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-29 10:39:25 -07:00
Nikolaj Bjorner c0694ae33a deal with memory leak during shutdown 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 10:39:07 -07:00
Nuno Lopes bc8cd7ff55 remove a few random mem allocs 2018-06-29 18:34:17 +01:00
Nikolaj Bjorner cbc5aaad2c strengthen simplification of to_int such that #1608 is handled during pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 09:44:54 -07:00
Nikolaj Bjorner 1e67717d75 log with unsigned characters to avoid malformed strings as in #1712 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 09:11:44 -07:00
Nikolaj Bjorner 7e29cc0b12 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-29 08:52:44 -07:00
Nikolaj Bjorner c429455f10 visit parameters during occurs count 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 08:52:25 -07:00
Nikolaj Bjorner 3da8fe4136
Merge pull request #1710 from agurfinkel/deep_space 
Deep space
 2018-06-28 16:57:02 -07:00
Arie Gurfinkel 9b578083f5 Avoid non-linear arithmetic in qgen 2018-06-28 16:50:43 -04:00
Arie Gurfinkel 5e87d7c4a3 Formatting: move q3 parameters closer together 2018-06-28 15:38:51 -04:00
Arie Gurfinkel bd63458778 Shuffle assumptions on every call 
Order of assumptions appears to make a huge difference on what lemmas
are discovered. Shuffling the assumptions ensures that the solver
is never stuck with any bad order.
 2018-06-28 15:38:51 -04:00
Arie Gurfinkel 6422fa3739 Fix arithmetic equality solver in qgen 2018-06-28 15:38:51 -04:00
Arie Gurfinkel 41a05e9d58 Add methods to print pob 2018-06-28 15:38:51 -04:00
Arie Gurfinkel a63e4b48ca Fix order of arguments when normalizing a conjunction 2018-06-28 15:38:51 -04:00
Arie Gurfinkel a8c9e3a837 Bug fix in qgen 2018-06-28 15:38:50 -04:00
Arie Gurfinkel e8e27f0daf Don't simplify bounds when normalizing a lemma 2018-06-28 15:38:50 -04:00
Nikolaj Bjorner f7512d6d5c
Merge pull request #1709 from nunoplopes/master 
MAM: check soft limits before calling the interpreter
 2018-06-28 10:31:00 -07:00
Nuno Lopes 46799cb3f0 MAM: check soft limits before calling the interpreter 2018-06-28 18:25:22 +01:00
Nikolaj Bjorner 18121e5241
Merge pull request #1707 from agurfinkel/deep_space 
Deep space
 2018-06-28 05:38:25 -07:00
Nuno Lopes 5de6628a5d remove spurious copies and inc_refs around ref_vector 2018-06-28 10:31:38 +01:00
Arie Gurfinkel 4abab8aaf5 Fix bug in qe_term_graph 
In merge, parents of A instead of parents of B were traversed.
Among other things, it created stale marks that caused an
infinite loop in to_lits()
 2018-06-27 22:54:55 -04:00
Arie Gurfinkel 0e5434ce0c Debug prints 2018-06-27 22:49:36 -04:00
Arie Gurfinkel 7c924c49f6 Do not evaluate quantified formulas in a model 2018-06-27 22:49:36 -04:00
Arie Gurfinkel 704c19920d Only 10 levels of weakness 2018-06-27 22:49:35 -04:00
Arie Gurfinkel 4339722e98 Fix segfaults in qgen 2018-06-27 22:49:35 -04:00
Arie Gurfinkel 49e9480928 Fix lemma_as_cti option 
Use negation of a lemma as a proof obligation. This speeds up discovering
bad lemmas that do not contain some reachable states.
 2018-06-27 22:49:35 -04:00
Arie Gurfinkel bc6604441b Helpers in model_core 2018-06-27 22:49:35 -04:00
Arie Gurfinkel d7234dc039 Inactive debug code 2018-06-27 22:49:35 -04:00
Arie Gurfinkel 2b4d92821a Avoid crashing on cancel 2018-06-27 22:49:35 -04:00
Arie Gurfinkel f6dcc6fc72 API to find pob in pob_manager 2018-06-27 22:49:35 -04:00
Arie Gurfinkel 5bc57238a6 Track whether pob is in pob_queue 
pob_queue is a priority queue. Changing a pob while it is in the queue might change
the priority. This is a source of subtle bugs. The flag is ment to help defend
against this issues in the future.

As a side-effect, a pob that is already in the queue will be silently not added
to it, and a new version of a pob might be created if a version being looked
for is already in the queue.
 2018-06-27 22:49:35 -04:00
Arie Gurfinkel c00c6b4285 Pobs are always managed 
Removed options to allow unmanaged pobs.
Other minor cleanups.
 2018-06-27 22:49:35 -04:00
Arie Gurfinkel 1910b4c87c Rename pobs into pob_manager 2018-06-27 22:49:35 -04:00
Arie Gurfinkel 176c0a97f7 Gracefully handle absence of a proof 2018-06-27 22:49:35 -04:00