z3 usage problem in java and strange error

Question

I am using Z3 for the constraints check, and I am currently use the java Z3 package.

What I am doing is that and this is my java code:

    Context context = new Context();
    Solver s=context.mkSolver();
    IntExpr i=context.mkIntConst("i");
    IntExpr zero=context.mkInt(1);//int i;
    BoolExpr initial=context.mkEq(i,zero);//i=0;
    IntExpr one=context.mkInt(1); //initial 1
    ArithExpr ipp=context.mkAdd(i,one);//i+1
    BoolExpr ippResult=context.mkEq(i,ipp);//i=i+1
    BoolExpr gtI=context.mkGe(i,zero);


    s.add(initial);
    s.add(ippResult);
    s.add(gtI);

    System.out.println(s+"\n\n");
 
    System.out.println(s.check());

And here is the output I have

  (declare-fun i () Int)
  (assert (= i 1))
  (assert (= i (+ i 1)))
  (assert (>= i 1))

   UNSATISFIABLE

So I don't know why z3 returns that it is not satisfiable? Since i+1>=1 actually, it is so strange. I don't know what code I am writing wrongly. Thanks!

Answer 1

Your program isn't complete; you use gtI but you never defined it. Probably cut-and-paste error.

In any case, your problem is nicely captured by the SMTLib portion of your output:

 (declare-fun i () Int)
 (assert (= i 1))
 (assert (= i (+ i 1)))
 (assert (>= i 1))

The second line says i is 1. Third line says i is equal to i+1. Combining these two, the solver deduces that it must be the case that 1 = 2. Which is clearly not true, and hence you get the UNSATISFIABLE result.

I suspect you wanted to create a new variable and use that in creating i+1, perhaps j? But hard to opine without knowing what it is that you are trying to achieve.