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 https://github.com/xapantu/counting-smt/issues/4, or mute the thread https://github.com/notifications/unsubscribe/ABbI08khB7qCJqKQbDjz_mMPjOyfiIYsks5qJLf-gaJpZM4IvcBg.