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

15 commits

Author SHA1 Message Date
Mikolas Janota 9df2a183d6 Adding translation to ackr_model_converter. 2016-06-06 18:06:45 +01:00
Nikolaj Bjorner 96e157e201 fix warnings for unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-17 13:54:22 -07:00
Christoph M. Wintersteiger 88f92660f0 Added param descrs collection to ackermannize_bv_tactic 2016-05-06 18:29:19 +01:00
Christoph M. Wintersteiger 16e487b32a Bugfix for ackermann helper 2016-04-08 17:20:09 +01:00
Christoph M. Wintersteiger bd0bd08ecf add is_considered_uninterpreted checks into acker_helper 2016-04-08 16:58:11 +01:00
Christoph M. Wintersteiger 405650c183 bugfix for ackr_model_converter (refcounts were off due to func_interps not being copied properly). 2016-04-01 13:17:48 +01:00
Mikolas Janota 217c0419a1 Avoiding adding a superfluous unary AND in lackr. 2016-03-29 19:34:30 +01:00
Mikolas Janota 363f57a2f4 Silently bailing out on quantifiers in lackr. 2016-03-29 19:19:07 +01:00
Mikolas Janota ae9f369574 Fix in lackr_model_constructor. 2016-03-10 17:36:05 +00:00
mikolas a2140085d6 In lazy ackermannization, collect all conflicting terms in one iteration. 2016-03-10 17:36:03 +00:00
Mikolas Janota 2f8465552c additional logging 2016-03-10 17:36:02 +00:00
Nikolaj Bjorner 4cd1efc50e address unused variable warnings from OSX build log 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-05 15:33:33 -08:00
Christoph M. Wintersteiger fa68b00563 Cleanliness 2016-02-10 14:39:33 +00:00
mikolas faa620f673 Further refactoring ackermannization. 2016-02-03 17:31:19 +00:00
mikolas f3240024e7 Further refactoring ackermannization. 2016-02-03 17:26:58 +00:00