mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity
14716 commits 24 branches 48 tags 158 MiB
Commit graph

14716 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
e8b506a172 update for nuget 2020-12-19 16:56:25 -08:00
Nikolaj Bjorner
4039785bb6 initial steps for including symbols 
@ahelwer - seems several steps are involved for enableing snupkg. I will try to see if I can get there. The NugetCommand@2 specifies whether to include symbols, but I haven't found the portion where it allows the user to specify the name of the package (to snukpg instead of nupkg).
 2020-12-19 16:44:05 -08:00
Nikolaj Bjorner
c022a3e573 fix reset break 2020-12-19 16:32:54 -08:00
Nikolaj Bjorner
28a6da4532 fix #4902 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-18 14:43:00 -08:00
Nikolaj Bjorner
8521d2caaa check engine configuration for unsupported engines #4898 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-18 14:38:42 -08:00
Nikolaj Bjorner
7ce1c38544 'na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-18 14:33:06 -08:00
Nikolaj Bjorner
e1f71d4932 fix #4904 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-18 14:32:16 -08:00
Nikolaj Bjorner
26af694d2c add overloads to != and == based on #4906 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-18 14:04:01 -08:00
Nikolaj Bjorner
fa5567fa1f fix #4905 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-18 14:00:05 -08:00
Nikolaj Bjorner
727095c563 fix #4899 2020-12-17 23:03:01 -08:00
Nikolaj Bjorner
11477f1ed1 fixes in new solver 
fix logging and lemma signs in arith_solver, move logging of drat equalities to euf
 2020-12-16 10:40:17 -08:00
Nikolaj Bjorner
26b4ab20db Update .gitignore 2020-12-14 17:34:02 -08:00
Nikolaj Bjorner
692bed7991 fix sign bug in internalization of literals 2020-12-14 17:33:14 -08:00
Nikolaj Bjorner
0ef8ebe89f fix #4895 2020-12-14 15:05:51 -08:00
Nikolaj Bjorner
7fe8298479 fix #4873 2020-12-12 16:03:48 -08:00
Nikolaj Bjorner
f71204c222 fix #4879 2020-12-12 13:37:25 -08:00
Nikolaj Bjorner
0643e7c0fc fix #4886 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-12 12:40:14 -08:00
Nikolaj Bjorner
dda4d66325 fix #4888 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-12 12:33:48 -08:00
Nikolaj Bjorner
8cb30d0505 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-12 12:21:34 -08:00
Nikolaj Bjorner
89fb55a864 fix #4890 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-12 12:20:53 -08:00
Nikolaj Bjorner
89a6c7a349 fix #4883 2020-12-10 07:30:19 -08:00
Lev Nachmanson
4d7062d2a1 fix in nla_ordered_lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-12-09 06:48:58 -08:00
Nikolaj Bjorner
621e99284b fix arith_solver=6 regression over solver=2 
https://github.com/Z3Prover/z3/issues/4613#issuecomment-668047545
 2020-12-08 16:36:43 -08:00
Nikolaj Bjorner
fae9481308 fix #4875 
remove unsound rewrite, regression
 2020-12-08 12:17:41 -08:00
Nikolaj Bjorner
97683bd48a fix #4876 2020-12-08 12:12:16 -08:00
Nikolaj Bjorner
8ce08d57a0 na 2020-12-08 12:08:15 -08:00
Nikolaj Bjorner
43ddb08332 fix #4874 2020-12-08 12:08:07 -08:00
Nikolaj Bjorner
9b9d906702 fix #4871 2020-12-07 22:07:30 -08:00
Nikolaj Bjorner
c49d39af81 perf for #4655 2020-12-07 21:34:57 -08:00
Nikolaj Bjorner
f5f980fa38 add rewrite rule 2020-12-07 21:28:23 -08:00
Nikolaj Bjorner
430b4ea252 fix #4870 2020-12-07 17:52:56 -08:00
Nikolaj Bjorner
9f6a0a868a fix #4389 fix #4859 
The bugs are duplicates
 2020-12-07 14:57:50 -08:00
Nikolaj Bjorner
409414c5b3 #4655 
rewrite replace using distributivity rule.
 2020-12-07 13:12:26 -08:00
Nikolaj Bjorner
289cc9de79 add rewrites for replace_all 2020-12-07 13:02:28 -08:00
Lev Nachmanson
7089610bbd set arith.cheap_eqsTO True 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-12-07 12:02:57 -08:00
Nikolaj Bjorner
bb3faf527c Update azure-pipelines.yml for Azure Pipelines 2020-12-07 10:34:50 -08:00
Nikolaj Bjorner
982da8db05 fix #4868 2020-12-07 10:27:00 -08:00
Nikolaj Bjorner
6c9bdc949e fix #4848 2020-12-07 05:59:55 -08:00
Nikolaj Bjorner
27dac3e1a0 fix #4844 2020-12-07 05:54:50 -08:00
Lev Nachmanson
b90143cc0e set the defalt for cheap_eqs=False, do not run 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-12-06 18:26:26 -08:00
Nikolaj Bjorner
4c1fcbaa62 fix #4865 2020-12-06 14:13:46 -08:00
Nikolaj Bjorner
746dd745ad fix #4856 2020-12-06 14:06:08 -08:00
Nikolaj Bjorner
c3c7aad1a8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-06 11:18:37 -08:00
Lev Nachmanson
2e5eb2dde2
Tree fix (#4864) 
* simplify cheap equality tree

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* simplify cheap equality tree

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* more fixes

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-12-06 11:18:27 -08:00
Alexey Vishnyakov
0c93c7ae03
Fix finding .git directory in CMake when z3 is a submodule of some other repository (#4850) 
* Fix finding .git directory in CMake when z3 is a submodule of some other repository

* Check that z3 is a submodule
 2020-12-05 18:27:35 -08:00
Addison Crump
b0cecf7747
Make multi-index arrays not so bad (#4857) 2020-12-05 15:45:46 -08:00
Nikolaj Bjorner
4d55f83654 misc 2020-12-04 16:59:13 -08:00
Murphy Berzish
b0fd25f041
z3str3: don't compute intersection difficulty against a null automaton (#4846) 2020-12-04 10:40:03 -06:00
Nikolaj Bjorner
6d427d9dae fix #4839 2020-12-02 12:46:24 -08:00
Nikolaj Bjorner
12198d13ac fix #4794 2020-12-02 12:24:35 -08:00