2

Could you tell me how to name assertions in a z3 SMT-LIB 2.0 benchmark? I would prefer to use the standard syntax of SMT-LIB, but as z3 seems not to understand it, I'm just looking for one working with z3. The need is to get unsat cores with labels.

Here is an example of benchmark I tested:

(set-option enable-cores)
(set-logic AUFLIA)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (! (<= 0 x) :named hyp1))
(assert (! (<= 0 y) :named hyp2))
(assert (! (<= 0 z) :named hyp3))
(assert (! (< x y) :named hyp4))
(assert (! (and (<= 0 y) (<= y x)) :named hyp5))
(assert (! (not (= x z)) :named goal))
(check-sat)
(get-unsat-core)

I am expecting the unsat core {hyp4, hyp5} because of the contradiction (x < y and y <= x), but z3 returns:

(error "ERROR: line 10 column 31: could not locate id  hyp1.")
(error "ERROR: line 11 column 31: could not locate id  hyp2.")
(error "ERROR: line 12 column 31: could not locate id  hyp3.")
(error "ERROR: line 13 column 30: could not locate id  hyp4.")
(error "ERROR: line 16 column 36: could not locate id  hyp5.")
(error "ERROR: line 18 column 35: could not locate id  goal.")
sat
()

I understand that z3 does not understand this way of naming, but I could not find another way in z3 documentation.

Could you help me please?

ygu
  • 345
  • 1
  • 16

1 Answers1

4

If I change your first command from

(set-option enable-cores)

to

(set-option :produce-unsat-cores true)

and that I then run your script:

z3 -smt2 script.smt2

I get as an output

unsat
(hyp4 hyp5)

which is I believe what you were expecting. Note that I'm using Z3 3.2 (for Linux, but that shouldn't make any difference).

Philippe
  • 9,582
  • 4
  • 39
  • 59
  • Thank you, but I tried this before, and I get same errors on unknown ids, plus this message: "(error "line 20 column 16: cores have not been enabled, use (set-option enable-cores)")", and this was the reason why I tried with the mentioned option. I think the version of z3 is the problem. I'm using Z3 2.19 for Linux. I'll go get your version and try. – ygu Oct 18 '11 at 13:23
  • 1
    Indeed: if you look at the [release notes](http://research.microsoft.com/en-us/um/redmond/projects/z3/releasenotes.html) you'll see that quite a few things have changed with respect to SMT-LIB 2.0 support since Z3 2.19. – Philippe Oct 18 '11 at 13:25
  • I just tried. It's working with Z3 3.2. Thank you again @Philippe. – ygu Oct 18 '11 at 13:35