SPF doesn't outputs counterexample when I use Choco solver with symbolic.optimizechoices is enabled

[kylekim72]

HI @yannicnoller , as we said SPF doesn't outputs it's counterexample if it has intermediate variable when asserts two nondeterministic variables are same. Here is source file and corresponding jpf configuration file.

package demo;


import org.sosy_lab.sv_benchmarks.Verifier;

public class NumericExample2 {

	public static void main(String[] args) {
		int a = Verifier.nondetInt();
		int b = Verifier.nondetInt();
		int c = a + 3;
		if(b != c) assert false;
	}

}

target=demo.NumericExample2
classpath=${jpf-symbc}/build/examples
sourcepath=${jpf-symbc}/src/examples

#symbolic.dp=z3bitvector
listener=.symbc.SymbolicListener
symbolic.optimizechoices = true
#search.multiple_errors=true
#symbolic.debug=true

In addition, here is screenshot of SPF's output.

As we discussed, the problem seems solver-dependent. When I use Z3, it doesn't happens.

When you have a moment, please reply to this issue. Thank you for your time!