Testing for long type symbolization

Hi I run the tests TestBitwiseLOR.jpf, but I am not able to switch the branching. It uses the latest versions of jpf-core and jpf-symbc.

TestBitWiseLOR.jpf:

target=gov.nasa.jpf.symbc.bitop.TestBitwiseLOR

classpath=${jpf-symbc}/build/tests

sourcepath=${jpf-symbc}/src/tests

symbolic.method= gov.nasa.jpf.symbc.bitop.TestBitwiseLOR.test(sym#sym)

symbolic.dp = cvc3bitvec

symbolic.debug=on

TestBitwiseLOR.java:

package gov.nasa.jpf.symbc.bitop;

public class TestBitwiseLOR {

    public void test(long x, long y) {
        long z = x | y;
        if(z == 0) {
            System.out.println("Branch one");
        } else {
            System.out.println("Branch two");
        }
    }

    public static void main (String[] args) {
        long x = 0;
        long y = 1;
        TestBitwiseLOR testLOR = new TestBitwiseLOR();
        testLOR.test(x, y);

    }

}

result:

====================================================== search started: 20/09/17 16:04
New sym int x_1_SYMINT min=-2147483648, max=2147483647
New sym int y_2_SYMINT min=-2147483648, max=2147483647
numeric PC: constraint # = 1
(y_2_SYMINT | x_1_SYMINT) < CONST_0 -> false

### PCs: total:1 sat:0 unsat:1

numeric PC: constraint # = 1
CONST_0 == (y_2_SYMINT | x_1_SYMINT) -> true

### PCs: total:2 sat:1 unsat:1

string analysis: SPC # = 0
NPC constraint # = 1
CONST_0 == (y_2_SYMINT | x_1_SYMINT)
Branch two
numeric PC: constraint # = 1
(y_2_SYMINT | x_1_SYMINT) > CONST_0 -> true

### PCs: total:3 sat:2 unsat:1

string analysis: SPC # = 0
NPC constraint # = 1
(y_2_SYMINT | x_1_SYMINT) > CONST_0
Branch two

Is this working correctly? My assumption is that the second constraint resolution will output Branch one. By the way, I can get the expected result by setting the variables used in TestBitwiseLOR.java to int type.

In other words, can't it be parsed correctly for long types? It would be very helpful if you could tell me the cause of the problem. If the cause is in SymbolicPathFinder, I would like to fix it myself and submit a PR.

Can someone give me some advice?

thank you.

SymbolicPathFinder / jpf-symbc

Testing for long type symbolization #55