search

usi-verification-and-security / opensmt

The opensmt solver
Other
78 stars 18 forks source link

Segfault on incorrect interpolation command #684

Open blishko opened 8 months ago

blishko commented 8 months ago

OpenSMT segfaults on the following SMT-LIB script:

(set-option :produce-interpolants 1)
(set-logic QF_LRA)

(declare-fun i1 () Real)

(assert (!(and (= i1 1.0)) :named A))
(assert (!(and (= i1 0.0)) :named B))

(check-sat)
(get-interpolants A)

The command (get-interpolants) should receive at least two partitions. We should be checking that and report error on malformed command, not segfault.