Fatal error: exception Not_found

[dddejan]

(set-logic QF_LIA)

(declare-fun x () Int)
(declare-fun y () Int)

(declare-fun c () Int)

(assert (= c (# u Int 
  (and 
    (>= u 0) 
    (>= 10 u)
    (= (+ u u) (+ x y))
  )
)))

(check-sat)
(get-model)

gives error

dejan@pup:~/workspace/counting-smt$ ./solver.native --verbose < ./examples/test04.smt2
 -> (set-logic QF_LIA)
 -> (declare-fun x () Int)
 -> (declare-fun y () Int)
 -> (declare-fun c () Int)
 -> (declare-fun card!1 () Int)
 -> (declare-fun card!2 () Int)
 -> (declare-fun card!3 () Int)
Fatal error: exception Not_found

[xapantu]

This requires multiplication, and is not supported at this moment.

On 06/06/2016 17:14, Dejan Jovanović wrote:

(set-logic QF_LIA)

(declare-fun x () Int)
(declare-fun y () Int)

(declare-fun c () Int)

(assert (= c (# u Int
(and
(>= u 0)
(>= 10 u)
(= (+ u u) (+ x y))
)
)))

(check-sat)
(get-model)

gives error

dejan@pup:~/workspace/counting-smt$ ./solver.native --verbose < ./examples/test04.smt2
-> (set-logic QF_LIA)
-> (declare-fun x () Int)
-> (declare-fun y () Int)
-> (declare-fun c () Int)
-> (declare-fun card!1 () Int)
-> (declare-fun card!2 () Int)
-> (declare-fun card!3 () Int)
Fatal error: exception Not_found

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
#4, or mute the thread
https://github.com/notifications/unsubscribe/ABbI08khB7qCJqKQbDjz_mMPjOyfiIYsks5qJLf-gaJpZM4IvcBg.