mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity
15875 commits 23 branches 48 tags 157 MiB
Commit graph

15875 commits

Author SHA1 Message Date
Nikolaj Bjorner da8530e2db 
That the bug went away is a fluke. It wasnt fixed.
It is in pb-preprocess, an essentially unused tactic. The special subsumption resolution rule wasn't accounting for membership of all variables.
 2021-08-02 09:03:15 -07:00
Nikolaj Bjorner e3be25dad6 2021-08-01 16:48:25 -07:00
Nikolaj Bjorner 123c446395 fix 2021-08-01 13:03:40 -07:00
Nikolaj Bjorner a4cc9e7895 2021-08-01 12:49:36 -07:00
Nikolaj Bjorner 924ea6ab31 again 2021-08-01 12:00:22 -07:00
Nikolaj Bjorner 50f5cafb50 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-01 05:09:58 -07:00
Nikolaj Bjorner 490dc66ec2 remove sine filter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-01 05:05:45 -07:00
Nikolaj Bjorner e148eea35d
Update wip.yml 2021-07-31 18:54:37 -07:00
Nikolaj Bjorner b3e63638f2
Update README.md 2021-07-31 18:02:13 -07:00
Nikolaj Bjorner 5b32c3778f remove out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 18:00:37 -07:00
Nikolaj Bjorner f5a08cc54e add wip 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 17:57:36 -07:00
Nikolaj Bjorner 55f5603714 remove coverage job from azure-pipeline as it is now in a self-contained action 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 17:17:00 -07:00
Nikolaj Bjorner eefde76bd4 na 2021-07-31 17:16:59 -07:00
Nikolaj Bjorner b723e1093b misc warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 17:16:59 -07:00
Nikolaj Bjorner ada873631e
Update coverage.yml 2021-07-31 14:56:20 -07:00
Nikolaj Bjorner 84e628cf74
Update coverage.yml 2021-07-31 13:49:37 -07:00
Nikolaj Bjorner 173257b4a0
Update coverage.yml 2021-07-31 13:15:11 -07:00
Nikolaj Bjorner efa82fa4f0
Update coverage.yml 2021-07-31 13:13:22 -07:00
Nikolaj Bjorner 42b3254c46
Update coverage.yml 2021-07-31 12:36:32 -07:00
Nikolaj Bjorner f17131fd06
Update coverage.yml 2021-07-31 12:01:39 -07:00
Nikolaj Bjorner 8f36287229
Update coverage.yml 2021-07-31 12:00:15 -07:00
Nikolaj Bjorner 2046907aaa
Update coverage.yml 2021-07-31 11:57:03 -07:00
Nikolaj Bjorner 07283ddea9
Update coverage.yml 2021-07-31 11:53:30 -07:00
Nikolaj Bjorner a2bd1d8fa2
Update coverage.yml 2021-07-31 11:51:00 -07:00
Nikolaj Bjorner 8b887cb0b8
Update coverage.yml 2021-07-31 11:46:26 -07:00
Nikolaj Bjorner ed27ce5526 fix regression in goal2sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 11:41:55 -07:00
Nikolaj Bjorner 7de8c72246 cleanups 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 11:32:47 -07:00
Nikolaj Bjorner 5533fc9dbc
Update README.md 2021-07-31 11:11:21 -07:00
Nikolaj Bjorner f6d6d2cc2d
Create coverage.yml 
Move coverage to self-contained github action
 2021-07-31 11:03:14 -07:00
Nikolaj Bjorner 6a9241ff0f 2021-07-31 11:00:12 -07:00
Nikolaj Bjorner e5401a4303 use quantifier 2021-07-31 00:32:43 -07:00
Nikolaj Bjorner 77cd82a5ca flatten if-then-else 2021-07-30 23:28:30 -07:00
Nikolaj Bjorner bcf0f671b8 disable drat inside of quantifier elaboration 2021-07-30 23:27:37 -07:00
Nikolaj Bjorner 6dfaaa43cd jobs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 22:38:56 -07:00
Nikolaj Bjorner 3f6a7748fa jobs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 22:38:16 -07:00
Nikolaj Bjorner ce23798cd0 coverage.yml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 22:36:14 -07:00
Nikolaj Bjorner 1e8009bbfc build/labels 2021-07-30 22:29:00 -07:00
Nikolaj Bjorner 53ab931626 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 21:35:09 -07:00
Nikolaj Bjorner 1488bf81ae 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 15:34:12 -07:00
Nikolaj Bjorner 31267e6ab8 2021-07-30 14:55:59 -07:00
Nikolaj Bjorner f3f83d0445 2021-07-30 13:43:02 -07:00
Nikolaj Bjorner 5ca8628e0d na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 13:42:54 -07:00
Nikolaj Bjorner 38250fc304 re-move 2021-07-29 15:33:30 -07:00
Nikolaj Bjorner b8a437bd8a 
relevancy propagation applies to quantifier unfolding.
 2021-07-29 15:05:06 -07:00
Nikolaj Bjorner 211a6c8752 rename 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-29 11:32:20 -07:00
Nikolaj Bjorner d0686671c5 Merge branch 'master' of https://github.com/z3prover/z3 2021-07-29 11:31:45 -07:00
Nikolaj Bjorner db5252a81b add dummy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-29 11:31:39 -07:00
0152la 72d3074a44
Add Ubuntu CMake Coverage CI step () 
Adds an extra step to CI jobs which executes the Z3 test suite with
coverage enabled, and additionally executed coverage-enhancing tests
added to z3test.
 2021-07-29 11:29:49 -07:00
Nikolaj Bjorner 703659a3a8 fix 2021-07-28 17:16:17 -07:00
Kiwamu Okabe 81b8f397b3
Need -thread option to compile OCaml example () 
I can compile the OCaml example with `-thread` option at Linux.

```
$ ocaml --version
The OCaml toplevel, version 4.05.0
```
 2021-07-28 16:57:26 -07:00