I am trying to use CVC4 to perform syntax-guided synthesis on a function. To begin, I am following CVC4 Getting Started and my example.smt2 file looks like this:
(set-logic ALL)
(declare-fun x () Int)
(assert (= (+ x x) (* x 2)))
(check-sat)
When I run cvc4 example.smt2 in command line in the directory, there should not be a problem based on the tutorial linked above. However, I get this error:
(error "Couldn't open file: example.smt2")
Note that this error is not the same as if the file does not exist. For example, when I run cvc4 exampl.doesnotexist, the following error occurs:
CVC4 Error:
Couldn't open file: exampl.doesnotexist
Which is different. I looked this up everywhere but could not find an answer. Any ideas?
You'll get this error if you don't have read-permissions on the file:
$ cat example.smt2
(set-logic ALL)
(declare-fun x () Int)
(assert (= (+ x x) (* x 2)))
(check-sat)
$ cvc4 example.smt2
sat
$ chmod u-r example.smt2
$ cvc4 example.smt2
(error "Couldn't open file: example.smt2")
$ cat example.smt2
cat: example.smt2: Permission denied
$ chmod u+r example.smt2
$ cat example.smt2
(set-logic ALL)
(declare-fun x () Int)
(assert (= (+ x x) (* x 2)))
(check-sat)
$ cvc4 example.smt2
sat
Depending on your operating system, simply allow read access and the problem should go away.