fzn2smt solver answers with `unknown` on tested formulas

Question

The fzn2smt tool allows one to solve flatzinc formulas via Yices.

When I try to run it, the solver answers with UNKNOWN to every formula I test. e.g.:

~$ java -Xmx4096M fzn2smt -ce "./yices-2.5.2/bin/yices -f" -i 2DPacking.fzn 
Time1:170
=====UNKNOWN=====

However, on the given example, it seems to correctly create the 2DPacking.fzn.smt instance in the same directory of the 2DPacking.fzn file:

~$ ls
2DPacking.fzn.smt    2DPacking.fzn    2DPacking.mzn    2DPacking.ozn

If I manually run Yices over the smt formula, I get a positive result:

~$ yices-smt -f 2DPacking.fzn.smt 
sat

(= x____00002_6_ 0)
...

IMPLICANT:
(>= x____00003_4_ 0)
...

Q: Does anyone else have experience with fzn2smt and know how to fix this issue?

---

Just to be sure that the issue I am experiencing is not due to the installation part, I will share it here:

 main_dir
 main_dir/fzn2smt-2-0-02      # unpacked fzn2smt files
 main_dir/antlr               # unpacked antlr-runtime-3.5 files
 main_dir/yices-2.5.2         # unpacked yices files

I also modified the environment variables as requested by the tool instructions:

 PATH=${main_dir}/yices-2.5.2/bin/:${PATH}
 PATH=${main_dir}/fzn2smt-2-0-02/:${PATH}

 CLASSPATH=${main_dir}:${CLASSPATH}
 CLASSPATH=${main_dir}/antlr:${CLASSPATH}
 CLASSPATH=${main_dir}/fzn2smt-2-0-02:${CLASSPATH}

Answer 1

As @Dekker suggested in the comments, the issue is due to fzn2smt seemingly not being updated in a while.

After some trials and errors, I found out that the most recent version of Yices that appears to be compatible with fzn2smt is version 2.2.1.

It can be executed as follows:

~$ java -Xmx4096M fzn2smt -ce "./yices-2.2.1/bin/yices-smt -f" -i 2DPacking.fzn
Time1:162
Time: 207
Pos: 0
item = array2d(1..2, 1..4, [0, 0, 0, 0, 1, 1, 1, 1]);
obj = 1;
----------
Time: 223
Pos: 0
item = array2d(1..2, 1..4, [0, 0, 0, 0, 1, 1, 1, 1]);
obj = 1;
----------
==========
Time2:228

---

Originally, fzn2smt was coupled with version 2 of Yices presented at the SMT-COMP 2009. To use that version, the command-line instruction to use the tool is slightly different:

~$ java -Xmx4096M fzn2smt -ce "./yices2smt09/bin/yices -f" -i 2DPacking.fzn
Time1:160
Time: 208
Pos: 0
item = array2d(1..2, 1..4, [0, 0, 0, 0, 1, 1, 1, 1]);
obj = 1;
----------
==========
Time2:223

Notice that

• the executable is named yices here, rather than yices-smt

• the output is slightly different, for some reasons the solution is printed more than once when using the newer version of the tool

---

Old versions of Yices can be downloaded from here.