Describe the bug
When calling get-value on a Boolean constant, cvc5 prints an error message and does not return a Boolean value. Specifically, for the following input:
(set-option :produce-models true)
(set-logic UFLIA)
(declare-sort F 2)
(declare-fun _select_1 ((F Int Int) Int) Int)
(declare-fun A () (F Int Int))
(declare-fun b () Bool)
(assert (and (= 1 (_select_1 A 1))
(= 0 (_select_1 A 0))
(= b (forall ((X1 Int))
(or (not (and (<= 0 X1) (< X1 4)))
(and (<= 0 (_select_1 A X1))
(<= (_select_1 A X1) 3)))))))
(check-sat)
(get-value (b))
cvc5 outputs:
sat
Could not evaluate (forall ((X1 Int)) (let ((_let_1 (_select_1 A X1))) (or (not (>= X1 0)) (>= X1 4) (and (>= _let_1 0) (not (>= _let_1 4)))))) in getValue.
((b (forall ((X1 Int)) (let ((_let_1 (_select_1 A X1))) (or (not (>= X1 0)) (>= X1 4) (and (>= _let_1 0) (not (>= _let_1 4))))))))
Command line arguments: None
cvc5 version/commit: 1e7433d
Operating system: Ubuntu 24.04
Describe the bug
When calling
get-valueon a Boolean constant, cvc5 prints an error message and does not return a Boolean value. Specifically, for the following input:cvc5 outputs:
Command line arguments: None
cvc5 version/commit: 1e7433d
Operating system: Ubuntu 24.04