Bug in OpenSMT or my fault?

[Joost Kraaijeveld]

Hi,

This small script from the tutorial by David Cok reports "sat" when run
with OpenSMT. I think however that it should report unsat (see comment).
Am I doing something wrong or is this a bug?

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(set-logic QF_UFIDL)

;(set-option :produce-models true)

(declare-fun x () Int)
(declare-fun y () Int)
(assert (= (+ x (* 2 y)) 20))
(assert (= (- x y) 2))
(assert (= x 2)) ; should unsat, x = 8, y = 6 is the only solution

(check-sat)

;(get-value ( x y ))

(exit)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

TIA

BTW: Yices with smtlib2parser-1.2 reports "unsat" as expected.

--
Groeten,

Joost Kraaijeveld
Askesis B.V.
Molukkenstraat 14
6524NB Nijmegen
tel: 024-3888063 / 06-51855277
fax: 024-3608416
web: www.askesis.nl

[Roberto]

Hi,

> (set-logic QF_UFIDL)
[...]

> (assert (= (+ x (* 2 y)) 20))

the problem is that you are using QF_UFIDL logic, but

x + 2y = 20

is not an IDL atom

R

[Joost]

On Oct 13, 5:08 pm, Roberto <roberto.bruttome...@gmail.com> wrote:
>
> x + 2y = 20
>
> is not an IDL atom

Ooops. You are right. I misread IDL: + and - are no *.

Thanks,

Joost