Example #3 in README.md is broken.

[rafaelbailo]

Running

using Satisfiability

@satvariable(x, Bool)
@satvariable(y, Bool)
@uninterpreted(f, Bool, Bool)

# Yices requires setting the logic manually. Here we set it to "QF_UFLIA" - "Quantifier free uninterpreted functions, linear integer arithmetic".
status = sat!(distinct(x, y), f(x) == y, f(f(x)) == x, solver=Yices(), logic="QF_UFLIA")
println("status = \$status")

yields the error

ERROR: IOError: could not spawn `yices-smt2 --interactive --smt2-model-format`: no such file or directory (ENOENT)
Stacktrace:
  [1] _spawn_primitive(file::String, cmd::Cmd, stdio::Vector{Union{RawFD, IO}})
    @ Base ./process.jl:128
  [2] #784
    @ ./process.jl:139 [inlined]
  [3] setup_stdios(f::Base.var"#784#785"{Cmd}, stdios::Vector{Union{RawFD, IO}})
    @ Base ./process.jl:223
  [4] _spawn
    @ ./process.jl:138 [inlined]
  [5] _spawn(::Base.CmdRedirect, ::Vector{Union{RawFD, IO}}) (repeats 3 times)
    @ Base ./process.jl:166
  [6] run(::Base.CmdRedirect; wait::Bool)
    @ Base ./process.jl:483
  [7] run
    @ ./process.jl:477 [inlined]
  [8] open(s::Solver)
    @ Satisfiability ~/rfs/rev/rev101_JOSS_Satisfiability/Satisfiability/src/call_solver.jl:134
  [9] talk_to_solver(input::String, s::Solver)
    @ Satisfiability ~/rfs/rev/rev101_JOSS_Satisfiability/Satisfiability/src/call_solver.jl:162
 [10] sat!(::BoolExpr, ::Vararg{…}; solver::Solver, logic::String, clear_values_if_unsat::Bool, line_ending::String, start_commands::String, end_commands::String)
    @ Satisfiability ~/rfs/rev/rev101_JOSS_Satisfiability/Satisfiability/src/sat.jl:50
 [11] top-level scope
    @ REPL[7]:1
Some type information was truncated. Use `show(err)` to see complete types.

[elsoroka]

I can't reproduce this issue...It might happen from not having Yices installed. Does the underlying command yices-smt2 --interactive --smt2-model-format work in the terminal? This was in the README to show that different solvers can be used. So I think a fix is to mention how to call the example with different solvers.

[rafaelbailo]

Does the underlying command yices-smt2 --interactive --smt2-model-format work in the terminal?

Indeed, it does not; I mistakenly assumed that because Z3 was installed automatically, the same would be true of Yices. Closing this.