I would suggest to split the Z3 package into multiple ones. As a quick idea I'd propose the following structure:

• Z3
  • Z3.Solver
  • Z3.Optimize

The reason for that is that our current spec has over 600 lines and the body has over 1300. It becomes more and more difficult to make changes, especially if they apply to both the public and private part of the spec since locating the code that needs to be modified becomes more tedious.

The "=" operator is currently used with its default implementation. This however seems to lead to wrong results sometimes. Instead Z3_is_eq_ast should be used.

Build z3 and our test suite with ASAN and enable resource leak checks:

   package Builder is                                                                                                   
      for Global_Compilation_Switches ("Ada") use ("-fsanitize=address", "-fno-omit-frame-pointer");      
   end Builder; 

   package Linker is                                                                                                    
      for Default_Switches ("Ada") use ("-lasan");                                                            
   end Linker; 

The default context is a source of error as it is not used consistently and as other contexts are not used consistently (sometimes an object is only created correctly when it is created in the default context).
Furthermore it becomes a difficulty when making the context a controlled type.

Since z3_mk_pow returns a real type and no integer (since negative powers may cause fractions) we have to support the real type. To keep the effort as low as possible only the functions that are required to properly identify the type and convert it error free to integers will be implemented. Operations using the real type itself are not in the scope of this ticket.

Currently Solver and Optimize are unconstrained types to enforce the usage of the create function. Due to these types being unconstrained we can't use them in records. However this is something we need. If we make these types unconstrained they will call Initialize when declared. Since we need a context for these types to be initialized properly we have to add an initialized property.

The Z3 C API uses manual reference counting. We currently do not care about reference counting, which likely results in memory leaks. To provide a usable API (without manual reference counting in Ada) we might have to use controlled objects for most of the types.

Each context and all its content must be kept in a single thread. To split a set of expressions into multiple threads they have to be moved to the respective context of the thread. This can be done by Z3_translate.

Currently we use Long_Integer and our own custom 64 bit unsigned type. I think we should use Ada.Interfaces and its Integer_n and Unsigned_n types instead since this improves compatibility to other code and prevents some parts of the code using AZ3 from just withing it for the unsigned type.

Create iterators for Z3 expressions to allow looping through their terms.

Support Z3_mk_solver_for_logic by adding a Logic parameter to the Create function.

In other projects some comparisons, even between simple expressions fail even if those expressions are equal. This happens differently in different Z3 versions.

For Z3 4.4.1 - 4.8.4: 6cadebf016729655fbc4d9434691eb4d91d3dc7e
For Z3 4.8.7+: 6e359057e0fc09afbb364c78b8744d3f20c6ad81

CI has not run since January ;(