Символьные строки JPF не генерируют ожидаемый ПК [Java Path Finder]

Question

Я пытаюсь запустить Jpf для символьных строк, но он не дает ожидаемого результата. Ниже приведена игрушечная программа, которую я пробую.

      import gov.nasa.jpf.symbc.Debug;
import static org.junit.Assert.*;

public class Toy {
public static void main(String args[]) {
    
    String s1,s2,s3;
    s1=Debug.makeSymbolicString("s1");
    s2=Debug.makeSymbolicString("s2");
    s3=Debug.makeSymbolicString("s3");
    
    checkEqual(s1,s2,s3);
}

static void checkEqual(String s1,String s2,String s3) {
    if(!s1.equals(s3)) 
        {
        if(!s2.equals(s3))  {
                
                System.out.println("s1.equals(s3)="+s1.equals(s3)+"\n");
                System.out.println("s2.equals(s3)="+s2.equals(s3)+"\n");
        }
    }
    System.out.println(Debug.getSolvedPC());
    }   
}

Файл .jpf выглядит следующим образом:

      target=Toy
classpath=${jpf-symbc}/build/examples
sourcepath=${jpf-symbc}/src/examples

symbolic.strings = true
symbolic.debug=true

Внутри вложенных условий if я печатаю значения сравнения строк, только когда строки s1, s2 не равны s3, только тогда должны быть напечатаны операторы печати. Я также распечатал ПК, используя symbolic.debug = true

Ниже приведен фрагмент вывода, в котором я сомневаюсь. Здесь вывод говорит, что s1, s2 равны и не равны s3 одновременно. Как это возможно? также в сообщении печати указано «s2.equals (s3) = true», тогда программа не должна входить в блок if.

      string analysis: SPC # = 4
(s2 equals s3) && (s1 equals s3) && (s2 notequals s3) && (s1 notequals s3)
NPC constraint # = 0
s2.equals(s3)=true

string analysis: SPC # = 4
(s2 equals s3) && (s1 equals s3) && (s2 notequals s3) && (s1 notequals s3) 
NPC constraint # = 0
constraint # = 0
## Warning: empty path condition
### PCs: total:9 sat:9 unsat:0

Код работает, когда я использую int вместо String. Было бы здорово, если бы вы могли мне помочь. Сообщите мне, если что-то не хватает в моей конфигурации jpf. заранее спасибо