mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity
13580 commits 23 branches 48 tags 157 MiB
Commit graph

13580 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 03d7a9acff #3581, bail out when smt solver gives up 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 17:19:57 -07:00
Nikolaj Bjorner 330b3cc8d6 fix #3584 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 16:50:53 -07:00
Nikolaj Bjorner 7f8738dd85 fix #3542 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 16:24:47 -07:00
Lev Nachmanson 3e845010dd replace v by j in lp printouts 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-30 15:59:03 -07:00
Nikolaj Bjorner a6e7ed039c fix #3587 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 15:18:37 -07:00
Nikolaj Bjorner 8a961a5ce9 fix #3554 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 15:02:55 -07:00
Nikolaj Bjorner 0ca5f59e35 fix #3550 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 14:45:38 -07:00
Nikolaj Bjorner fe81de6d39 fix #3555 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 14:37:38 -07:00
Nikolaj Bjorner b9dd18483c fix #3571 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 14:11:36 -07:00
Nikolaj Bjorner d4aa850412 fix #3572 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 14:09:47 -07:00
Nikolaj Bjorner e263f9b238 fix #3559 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 14:00:30 -07:00
Nikolaj Bjorner de2ad26826 fix #3568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 13:51:45 -07:00
Nikolaj Bjorner 04e51ffcb5 fix #3569 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 13:40:59 -07:00
Nikolaj Bjorner 53b5ca3c2b disambiguate call 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 13:35:40 -07:00
Nikolaj Bjorner 5152c9500d fix #3591 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 13:08:58 -07:00
Nikolaj Bjorner bf9779cb87 fix #3593 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 12:46:18 -07:00
Nikolaj Bjorner aeee44398d fix #3594 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 12:40:24 -07:00
Lev Nachmanson 7936df8e0b pass std::function as const aliases 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-30 12:20:47 -07:00
Nikolaj Bjorner ba4765f16f debugging #3511 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 11:00:02 -07:00
Nikolaj Bjorner f74079de01 fix #3529 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 11:00:02 -07:00
Nikolaj Bjorner c142f99127 fix #3532 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 11:00:02 -07:00
Nikolaj Bjorner 0b10cb3312 fix #3528 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 11:00:02 -07:00
Lev Nachmanson 9be7bda69a fix a bug in column patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-29 15:03:46 -07:00
Lev Nachmanson 7a950dd667 patch reals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-29 15:03:46 -07:00
Lev Nachmanson 3237bd9243 better tracing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-29 15:03:46 -07:00
Nikolaj Bjorner 7086a7c26a fix #3531 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-29 11:15:01 -07:00
Nikolaj Bjorner 1155db383e fix #3540 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-29 10:55:47 -07:00
Nikolaj Bjorner 9f386306ef na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-29 10:55:47 -07:00
Nikolaj Bjorner 1a995da0ae fix #3538, turn on proof checking assertions in goal.cpp for earlier coverage 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-29 10:55:47 -07:00
Lev Nachmanson 907d310600 get rid of arith.nla parameter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-27 14:33:40 -07:00
Lev Nachmanson f9151a7a8e correct the default options: smt.arith.nla=False 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-27 13:55:23 -07:00
Nikolaj Bjorner 4b7bd3a881 fix #3536 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-27 12:59:24 -07:00
Nikolaj Bjorner f8dcaa8885 'na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-27 10:23:00 -07:00
Lev Nachmanson 352f4b5b37 use u_set in random_update() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-26 18:11:32 -07:00
Nikolaj Bjorner 12f62e73d5 fix ordering of delayed assume eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 16:24:34 -07:00
Nikolaj Bjorner 7a04e52c41 fix ordering of delayed assume eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 16:22:24 -07:00
Nikolaj Bjorner 499843ae7f remove verbose 0 output, #3527 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 14:49:14 -07:00
Arie Gurfinkel 5673ec046b qe_term_graph fix for #3526 2020-03-26 16:45:06 -04:00
Nikolaj Bjorner d4699b181d fix assertion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 12:49:44 -07:00
Nikolaj Bjorner 73ab95d338 remove canonize in seq solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 12:47:30 -07:00
Nikolaj Bjorner 0fa04179d0 fix #3522 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 11:06:04 -07:00
Nikolaj Bjorner 5da2169a0e fix #3524 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 10:38:13 -07:00
Nikolaj Bjorner ee2e81b696 fix #3517 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 10:02:41 -07:00
Nikolaj Bjorner 493671aa72 fix #3520 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 09:58:06 -07:00
Nikolaj Bjorner 868a6b3594 fix #3521 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 09:44:00 -07:00
Nikolaj Bjorner 37f080b877 fix #3523 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 09:44:00 -07:00
Nikolaj Bjorner c165f69248 fix #3525 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 09:44:00 -07:00
Lev Nachmanson fd219abe8c fix test build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson b34f841421 setting the old defaul options for nla 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson f5b62015fc change the return type of ival.var() to tv 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00