Commit 8d7fbcb7 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Avoid NPE's when comparing the output from Z3. 

readLine can return a null.  To avoid an NPE, compare the string constant to
the output.  If null is returned, just throw an exception specifically about
this.
parent 31c7059b

src/main/java/ca/mcscert/jtet/smtlibchecker/CheckerRunner.java

+3 −3
Original line number Diff line number Diff line
@@ -105,7 +105,7 @@ final public class CheckerRunner { 
                z3Input.flush();



                String res = z3Output.readLine();

                if(res.equals("sat")) { // Failed query.  Get a the result.

                if("sat".equals(res)) { // Failed query.  Get a the result.

                    z3Input.write(GetValueRequestString);

                    z3Input.flush();
@@ -113,13 +113,13 @@ final public class CheckerRunner { 
                    result.Query = query;

                    result.SampleValues = parseSMTLIBOutput(z3Output);

                    ret.add(result);

                } else if(res.equals("unknown")) {

                } else if("unknown".equals(res)) {

                    // Z3 failed to prove.  Throw a failure to check for now.

                    CheckerRunnerResult result = new CheckerRunnerResult();

                    result.Query = query;

                    result.SampleValues = null;

                    ret.add(result);

                } else if(!res.equals("unsat")) {

                } else if(!"unsat".equals(res)) {

                    // Something went wrong

                    throw new IllegalStateException("Z3 outputed something wrong (" + res + ")!");

                }