java - JPF シンモリック文字列が期待される PC を生成しない [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 と等しくない場合にのみ、print ステートメントを出力する必要があります。また、symbolic.debug=true を使用して PC を印刷しました

以下は、私が疑問を持っている出力のスニペットです。ここで、出力は、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

String の代わりに int を使用すると、コードが機能します。助けていただければ幸いです。jpf 構成に何か不足があれば教えてください。前もって感謝します