3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Commit graph

13485 commits

Author SHA1 Message Date
Arie Gurfinkel 2b27aa1ce6 fix #3908 2020-04-11 13:58:10 -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
Nikolaj Bjorner 03e411c22d fix #3868
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-11 02:28:38 -07:00
Nikolaj Bjorner 21a31fcd26 add missing fixed propagations on negated integer inequalities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-11 02:28:38 -07: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
Nikolaj Bjorner fdabaa6cd2 fix #3807
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-10 13:43:00 -07: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
Nikolaj Bjorner d14ce97b76 multiple regressions from previous commit
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-10 12:18:30 -07:00
Nikolaj Bjorner b42b329d6c initialize best-phase-size #3897
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-10 12:04:55 -07:00
Nikolaj Bjorner 33677b9803 fix #3898
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-10 11:56:35 -07:00
Nikolaj Bjorner a7123062a0 fix #3899 regression from transitioning to decompose_monomial
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-10 11:22:12 -07:00
Nikolaj Bjorner 61fb134653 fix #3782
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-10 11:22:12 -07: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 ee9c797822 address #3886 and #3891 by revamping nl_arith decoupling of monomial analysis and access
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-10 01:33:46 -07:00
Nikolaj Bjorner addbe55823 fix #3846, another bug in eq2bv-tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-09 19:55:40 -07:00
Nikolaj Bjorner 066413516f disable temp debug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-09 19:39:31 -07: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
Lev Nachmanson bd3946677c resize m_var_set in random_update
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-09 14:45:32 -07:00
Nikolaj Bjorner cd98a21984 decouple random update with assume eqs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-09 14:01:34 -07:00
Nikolaj Bjorner 5ced73afb5 decouple random update with assume eqs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-09 14:00:31 -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 3cae0b450e fix #3887
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-09 12:03:02 -07:00
Nikolaj Bjorner e14bca2ebf more graceful behavior of seq.validate #3885
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-09 11:59:25 -07:00
Lev Nachmanson 5d3b00b5ea build fix
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-09 11:47:32 -07:00
Lev Nachmanson 57f622acc1 fixes in random_update()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-09 11:47:32 -07:00
Nikolaj Bjorner f04dfa71a6 be a bit more graceful in failing validation #3883
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-09 11:38:06 -07:00
Nikolaj Bjorner def2de69f4 fix #3882 ?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-09 11:31:29 -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
Lev Nachmanson 21b7dc627e create a more precize lemma for the empty intersection case
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-09 10:26:37 -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 6eebfd0629 fix #3880
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-08 18:10:12 -07:00
Nikolaj Bjorner 56358a6b94 fix #3867
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-08 18:06:37 -07:00
Nikolaj Bjorner 4bfcc75ed4 fix #3869
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-08 17:18:55 -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 77e7dcb3c3 fix #3874
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-08 16:32:57 -07:00
Nikolaj Bjorner 52df98f9ca na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-08 16:31:47 -07:00
Nikolaj Bjorner 4532b07e88 guard against untempered parameter combinations #3877
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-08 16:26:11 -07:00
Nikolaj Bjorner e1d2480a8b fix #3860 fix #3861
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-08 16:26:11 -07:00
Lev Nachmanson c5e08f0444 add dependencies lost in case of an empty intersection
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-08 15:47:15 -07:00
Lev Nachmanson 4621767968 handle the empty intersection in nla_intervals
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-08 15:47:15 -07:00