Using Proofs

[alpaylan]

I am trying to write a simple verification backend using z3.rs, I have the statements below. assertions: (= y (bvmul x #x0000000000000003)) assertions: (= x (bvadd x x)) negated goal: (not (= (bvadd x x) (bvmul x #x0000000000000003)))

So my expectation is that the solver comes up with SAT result, yet I get UNSAT.

I wanted to understand why it does that, so I tried extracting the proof, yet I could not find any useful method that proof uses which I can inspect the process. The code examples are not very useful either, if anyone could post anything allowing me to move forward, I would be grateful.

[sameer]

Hey there, could you share your rust code? The examples are indeed a bit lacking, I'd recommend looking at the tests.

Also, doesn't your second assertion x = x + x, mean x can only be 0 and your goal ! (x+x = 3x) won't be SAT?

[alpaylan]

You are actually right, my problem was that I looked at the first 2 assertions as assignments rather than equality constraints, my bad. So in fact the root cause of the issue is solved, I did not close it because I think we should still be able to inspect the "proof" object, which might not be necessary in this case, but will probably be required in future.

It seems like even a simple #derive[(debug)] could help with that, what do you think?

Also, I checked with tests, they also did not have any cases where proof is used.

[GreenBeard]

@alpaylan Here is an example for how to see a proof (not that it is very readable). It attempts to claim that 2 + 3 = 6, and then when given a counterproof it prints it out.

fn test_a(context: &z3::Context) {
  /* assert 2 + 3 = 6 */
  let solver: z3::Solver = z3::Solver::new(context);
  let a: z3::ast::Int = z3::ast::Int::from_u64(context, 2);
  let b: z3::ast::Int = z3::ast::Int::from_u64(context, 3);
  let c: z3::ast::Int = z3::ast::Int::add(context, &[ &a, &b ]);
  let d: z3::ast::Int = z3::ast::Int::from_u64(context, 6);

  solver.assert(&c._eq(&d));

  let result: z3::SatResult = solver.check();
  print!("Result: {:?}\n", result);
  if let z3::SatResult::Unsat = result {
    let proof = solver.get_proof();
    print!("{:?}\n", proof);
  }
}

Edit: If this answers your issue of not being able to "inspect the 'proof' object" then feel free to close the issue.