search

xapantu / counting-smt

1 stars 1 forks source link

Fatal error: exception Smtlib.Not_allowed("1") #6

Closed dddejan closed 8 years ago

dddejan commented 8 years ago 
(set-logic QF_LIA)

(declare-fun s1 () Int)
(declare-fun s2 () Int)

(assert (= s1 (# u Int (and (>= u 1) (>= 2 u)))))
(assert (= s2 (# u Int (and (>= u 1) (>= 2 u) (>= s1 (+ u 1))))))

(check-sat)
(get-model)

Don't want to over do it with issues so I'll stop here. The language doesn't support constants, anything other that >=, and there is no negation.

xapantu commented 8 years ago

Yes, I've not tested that code enough… sorry about that.