SPF doesn't print out a PathCondition

[kylekim72]

Hi, I'm posting this issue since SPF doesn't print out a PathCondition for certain benchmark. I'm using gradle-build branch's SPF.
When I run SPF with jpf-sv-comp script on jpf-regression/ExSymExe11_false, SPF provides correct result, but there is no PathCondition.

Here is the part of the script that creates .jpf configuration file(the difference is that it utilizes SymbolicListener).

# create configuration file
echo "target=Main" > $DIR/config.jpf
echo "classpath=`pwd`/jpf-symbc/build/classes:$DIR/target/classes" >> $DIR/config.jpf
echo "symbolic.dp=z3bitvector" >> $DIR/config.jpf
echo "symbolic.bvlength=64" >> $DIR/config.jpf
echo "search.depth_limit=200" >> $DIR/config.jpf
echo "symbolic.strings=true" >> $DIR/config.jpf
#echo "symbolic.optimizechoices=false" >> $DIR/config.jpf
#echo "symbolic.string_dp=z3" >> $DIR/config.jpf
#echo "symbolic.string_dp_timeout_ms=3000" >> $DIR/config.jpf
echo "symbolic.lazy=on" >> $DIR/config.jpf
echo "symbolic.arrays=true" >> $DIR/config.jpf
echo "listener = .symbc.SymbolicListener" >> $DIR/config.jpf

In addition, here is a source file of program :

/*
 * Origin of the benchmark:
 *     repo: https://babelfish.arc.nasa.gov/hg/jpf/jpf-symbc
 *     branch: updated-spf
 *     root directory: src/tests/gov/nasa/jpf/symbc
 * The benchmark was taken from the repo: 24 January 2018
 */
/*
 * Copyright (C) 2014, United States Government, as represented by the
 * Administrator of the National Aeronautics and Space Administration.
 * All rights reserved.
 *
 * Symbolic Pathfinder (jpf-symbc) is licensed under the Apache License,
 * Version 2.0 (the "License"); you may not use this file except
 * in compliance with the License. You may obtain a copy of the License at
 *
 *        http://www.apache.org/licenses/LICENSE-2.0.
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */

// package gov.nasa.jpf.symbc;
import org.sosy_lab.sv_benchmarks.Verifier;

public class Main {
  static int field;

  public static void main(String[] args) {
    int x = 3; /* we want to specify in an annotation that this param should be
                  symbolic */

    Main inst = new Main();
    field = Verifier.nondetInt();
    inst.test(x, field);
    // test(x,x);
  }
  /* we want to let the user specify that this method should be symbolic */

  /*
   * test IMUl, INEG & IFGT bytecodes
   */
  public void test(int x, int z) {
    System.out.println("Testing ExSymExe11");
    int y = 3;
    z = -x;
    x = z * x;
    if (z <= 0) System.out.println("branch FOO1");
    else System.out.println("branch FOO2");
    if (y <= 0) System.out.println("branch BOO1");
    else {
      System.out.println("branch BOO2");
      assert false;
    }

    // assert false;
  }
}

Finally, run jpf-sv-comp inside SPF directory like this : ./jpf-sv-comp.sh --propertyfile /path/to/assert_java.prp /path/to/java/common /path/to/jpf-regression/ExSymExe11_false. Here is an example screenshot :

After you run this command, SPF outputs UNSAFE, but there is no PathCondition and as you can see, the method summary is empty. Here is screenshot of output :

Please check this problem when you have a moment. Thank you for your time!