CODEWITHSUNDEEP
z3
Raj
Raj

Reputation: 3462

Migrating from Z3 Version 3.2 to Version 4.0

I am migrating from Z3 version 3.2 to version 4.0. However, the code which was working earlier, no longer works directly and I am trying to find out the reasons for the same. I reduced the entire code to a very simple declaration and assertion, still it won't work. The code is - 

long intSort = Z3_mk_int_sort (context);
long periodDeclStr = Z3_mk_string_symbol(context, "period");
long periodVar =  Z3_mk_const(context, periodDeclStr, intSort);

long solver = z3_mk_solver();
long zero = Z3_mk_int (context, 0, intSort);
long eqSt = Z3_mk_eq(context, periodVar, zero);     
Z3_solver_assert (context, solver, eqSt);

The problem is with the second last statement Z3_mk_eq()

I receive the error as -

WARNING: invalid function application, sort mismatch on argument at position 2
WARNING: (define = arith arith Bool) applied to: 
period of sort arith
0::Int of sort Int

My Questions are as follows -

  1. How to debug this error? This is still working with version 3.2, without solver though.
  2. Is it necessary that I must create solver only after I finished adding variables to the context? Can I add variables to the context after creating the solver? Or I have to re-create the solver?

Sorry for the trouble. I was mixing up solver and context to pass them to the solver. However, the problem still remains the unsolved. I am having a crash in Z3_ast_to_String() API. I will try to resolve the problem and post the update.

Upvotes: 1

Views: 236

Answers (2)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

There is an interaction log now with Z3 4.0 that records the API interaction precisely. It should be possible use this feature to debug the JNI layering and the bugs you find. The log is opened using Z3_open_log(). You should open the log before creating any contexts. You can close the log at any point as well (Z3_close_log()) if you only want to capture a subset of the interaction. You can replay the log by giving the the suffix ".log" and run Z3 on it. Alternatively, you can run Z3 with the option /log, that is, "Z3.exe /log " to replay the interaction.

Upvotes: 3

Josh Berdine
Josh Berdine

Reputation: 326

Don't you want Z3_mk_eq(context, id, zero) instead of Z3_mk_eq(context, periodDecl, zero)?

Upvotes: 0

Related Questions