Commit 0a384c0a authored by Matthew Dawson's avatar Matthew Dawson
Browse files

In Z3, handle an unknown result for check-sat. 

If an unknown error is received, treat it as a failure but without sample
values.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@11085 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent af7b830c

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/smtlibchecker/CheckerRunner.java

+6 −0
Original line number Diff line number Diff line
@@ -98,6 +98,12 @@ final public class CheckerRunner { 
                    result.Query = query;

                    result.SampleValues = parseSMTLIBOutput(z3Output);

                    ret.add(result);

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

                    // 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")) {

                    // Something went wrong

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