mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity
13904 commits 23 branches 48 tags 157 MiB
Commit graph

950 commits

Author SHA1 Message Date
Hari Govind V K
ed92b8437c
fix #4054 (#4277) 
* flag when quantified lemmas are added to smt_context

* When solver returns unknown but cannot create child, return unknown

* handle unknowns when qlemmas and weak_abs are turned on
 2020-05-21 09:58:09 -07:00
Nikolaj Bjorner
09d881cce5 na 2020-05-02 15:54:12 -07:00
Nikolaj Bjorner
75859ef4e4 model anomaly fix #4171 2020-05-02 15:53:46 -07:00
Nikolaj Bjorner
397bf2dec6 move windows dependencies down 2020-04-30 19:31:11 -07:00
Hari Govind V K
dbfa3dd7f1
[spacer] implement spacer::is_clause() (#4170) 
Spacer has a different defintion of is_clause() than ast_util.
It is currently only used in assertions.

Main difference:
  x=y
where x and y are Bool atoms is considered to be an atom, so that
(or (= x y) (not (= z y)))
is a literal

Co-authored-by: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
 2020-04-30 14:03:48 -07:00
Nikolaj Bjorner
e67112f289 NYI control paths 2020-04-28 20:19:20 -07:00
Nikolaj Bjorner
a0de244487 pleay nice with alignment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-26 23:29:42 -07:00
Nikolaj Bjorner
a884201d62 remove using insert_if_not_there2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-25 15:08:51 -07:00
Nikolaj Bjorner
caa5b09046 fix #4050 - have to delay model compression because it may use internal symbols that have to be transformed. model compression is used prior to displaying certificate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-22 13:33:36 -07:00
Nikolaj Bjorner
eded7d023d fix #4006 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-19 16:00:03 -07:00
Nikolaj Bjorner
dd3e574f81 fix #3983 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-16 14:03:06 -07:00
Nikolaj Bjorner
f67077b7ff warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-15 17:13:02 -07:00
Nikolaj Bjorner
7ed9996fc0 fix #3962 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-14 11:05:05 -07:00
Nikolaj Bjorner
299a6f4aee fix #3939 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-13 14:00:21 -07:00
Nikolaj Bjorner
d3db2af81d fix #3941 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-13 13:15:15 -07:00
Nikolaj Bjorner
97af74d8cb fix #3917 remove non-native mode for recfun 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-11 14:19:26 -07:00
Lev Nachmanson
ec0cd644f1 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-11 12:28:54 -07:00
Arie Gurfinkel
20d72e5d97 (spacer) fix (get-proof) to return proper refutations 2020-04-11 14:38:27 -04:00
Arie Gurfinkel
1f6815213d spacer: fail with exception on quantifiers in recursive rules 2020-04-11 14:16:47 -04:00
Arie Gurfinkel
1e96570365 fix #3915 2020-04-11 14:16:29 -04:00
Arie Gurfinkel
f821ee38e5 Fix #3907 
Protect spacer from existential quantifiers in the tail.

Some transformations seem to introduce existentially quantified terms.
 2020-04-11 11:21:13 -04:00
Arie Gurfinkel
337c07a44c Fix #3788 by converting assert into a throw 2020-04-11 09:15:32 -04:00
Arie Gurfinkel
ae5a713e81 fix #3906 by fixing a regression from today 2020-04-11 00:18:25 -04:00
Arie Gurfinkel
136b0b23ce address #3905 2020-04-11 00:03:13 -04:00
Arie Gurfinkel
d53e30ecbe finished fix for #3849 by converting assert into trace 2020-04-10 21:10:39 -04:00
Arie Gurfinkel
fa900c39ab hide fp.xform.scale 2020-04-10 15:46:59 -04:00
Arie Gurfinkel
a261bd94ed silence #3788 
better proof generation for the case when the query is reachable from initial
states. This case needs to be handled better so that spacer can assume
the problem is non-trivial.
 2020-04-10 15:21:47 -04:00
Arie Gurfinkel
b1b77e57e1 (partial) fix #3788 
Fixes a bug in computation of implicants inside spacer.
The instance now returns `unknown`. The root cause is the difference in what
proofs are in spacer and SMT. Spacer returns a proof of query, but horn_tactic
expects a proof of FALSE.
 2020-04-10 12:26:31 -04:00
Arie Gurfinkel
44302f3f2a fix #3646 2020-04-10 10:01:14 -04:00
Nikolaj Bjorner
1fce2905ec fix #3832 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-09 19:38:08 -07:00
Nikolaj Bjorner
c4b52edb29 add back assertion for #3849 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-09 18:08:40 -07:00
Nikolaj Bjorner
4651bffafc fix #3831 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-09 17:45:05 -07:00
Nikolaj Bjorner
76ac9917c8 fix #3890 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-09 13:12:37 -07:00
Nikolaj Bjorner
cc794a19bc more on #3858 elim_term_ite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-09 10:31:34 -07:00
Nikolaj Bjorner
99c328b6ef more fixes for #3858 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-09 09:52:15 -07:00
Nikolaj Bjorner
8cf5a7525b fix #3858 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-09 09:22:02 -07:00
Nikolaj Bjorner
2673807a7f fix #3863 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 18:34:15 -07:00
Nikolaj Bjorner
9f1a2e2c94 fix #3872 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 17:12:14 -07:00
Nikolaj Bjorner
db3d6d7c95 fix #3879 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 17:05:29 -07:00
Nikolaj Bjorner
6e8d9001dc fix #3843 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 11:08:45 -07:00
Nikolaj Bjorner
40aa2f7cb2 fix 3838 fix #3837 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 05:49:24 -07:00
Nikolaj Bjorner
7595371721 fix #3834 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 04:56:15 -07:00
Nikolaj Bjorner
dde0c9bd0d fix #3833 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 04:34:36 -07:00
Nikolaj Bjorner
bd59fceaec na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 03:48:38 -07:00
Nikolaj Bjorner
7722bf1a55 declutter spacer_manager 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 03:35:58 -07:00
Nikolaj Bjorner
8e6bb30c82 cleanup bit2bool from models #3847 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 03:06:01 -07:00
Nikolaj Bjorner
0e78f092b5 fix #3849 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-07 19:28:02 -07:00
Nikolaj Bjorner
7fc9eb11db fix #3850 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-07 19:22:50 -07:00
Nikolaj Bjorner
6e7e53e25c block selected configurations from HORN tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-07 19:14:01 -07:00
Nikolaj Bjorner
35f184a6b9 fix #3826 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-07 14:39:54 -07:00