Unsound? smtlib2 output

[leepike]

SAW appears to generate inconsistent SMTLIB2 files: a smtlib file returns unsat in the case SAW returns Valid and a smtlib file returns unsat in the case SAW returns Invalid.

Possibly related to #489

> cat Double.java
class Double {
    public static int add(int x, int y) {
        return x + y;
    }

    public static int dbl(int x, int y) {
        return x - y;
    }
}

> cat double_java.saw
enable_experimental;

j <- java_load_class "Double";
add <- crucible_java_extract j "add";
dbl <- crucible_java_extract j "dbl";

let thm = {{ \x y -> add x y == dbl x y }};
write_smtlib2 "java_double.smt2" thm;

result <- prove abc thm;
print result;

print "Done.";

> javac Double.java
> saw -j <path>/rt.jar java_double.saw
Loading file "java_double.saw"
extracting add
extracting dbl
prove: 1 unsolved subgoal(s)
Invalid: [x = 671088640, y = 67108864]
Done.

> z3 java_double.smt2
...
unsat 

Now let's change Double.java to make the functions equivalent:

> cat Double.java
class Double {
    public static int add(int x, int y) {
        return x + y;
    }

    public static int dbl(int x, int y) {
        return x + y;
    }
}

> javac Double.java
> saw -j <path>/rt.jar java_double.saw
Loading file "java_double.saw"
extracting add
extracting dbl
Valid
Done.

> z3 java_double.smt2
...
unsat