Projects >> WhileyCompiler >>acd6b75b1a331aa8064b26f6113b9037fe3b83f5

Chunk
Conflicting content 
     * wycs.solver.smt.Stmt.DefineSort} and {@link wycs.solver.smt.Stmt.Assert}s. Doing this means
     * we don't have to manually check for their existence and ensures they are uniquely defined.
     */
<<<<<<< HEAD
    private final Set elements = new LinkedHashSet<>();
=======
    private final Set lines = new LinkedHashSet();
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123

    /**
     * Appends the given elements to this block.
Solution content 
     * wycs.solver.smt.Stmt.DefineSort} and {@link wycs.solver.smt.Stmt.Assert}s. Doing this means
     * we don't have to manually check for their existence and ensures they are uniquely defined.
     */
    private final Set elements = new LinkedHashSet<>();

    /**
     * Appends the given elements to this block.
File
Block.java
Developer's decision
Version 1
Kind of conflict
Attribute
Method invocation
Chunk
Conflicting content 
     * wycs.solver.smt.Stmt.DefineSort} and {@link wycs.solver.smt.Stmt.Assert}s. Doing this means
     * we don't have to manually check for their existence and ensures they are uniquely defined.
     */
<<<<<<< HEAD
    private final Set elements = new LinkedHashSet<>();
=======
    private final Set lines = new LinkedHashSet();
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123

    public Smt2File() {}
Solution content 
     * wycs.solver.smt.Stmt.DefineSort} and {@link wycs.solver.smt.Stmt.Assert}s. Doing this means
     * we don't have to manually check for their existence and ensures they are uniquely defined.
     */
    private final Set elements = new LinkedHashSet<>();

    public Smt2File() {}
File
Smt2File.java
Developer's decision
Version 1
Kind of conflict
Attribute
Method invocation
Chunk
Conflicting content 
         * {@inheritDoc}
         */
        @Override
<<<<<<< HEAD
        public List generateInitialisers() {
            List initialisers = new ArrayList<>();

            initialisers.addAll(generateSorts());
            initialisers.addAll(generateAddFunctions());
            initialisers.addAll(generateContainsFunctions());
            initialisers.addAll(generateRemoveFunctions());
            initialisers.addAll(generateEmptyConstants());
            initialisers.addAll(generateLengthFunctions());
            initialisers.addAll(generateEmptyLengthAssertions());
            initialisers.addAll(generateSubsetFunctions());
            // Causes lots of the tests to timeout
            //            initialisers.addAll(generateSubsetLengthAssertions());

            return initialisers;
=======
        public List generateLines() {
            List lines = new ArrayList();

            lines.addAll(generateInitialisors());
            lines.addAll(generateAddFunctions());
            lines.addAll(generateContainsFunctions());
            lines.addAll(generateRemoveFunctions());
            lines.addAll(generateEmptyConstants());
            lines.addAll(generateLengthFunctions());
            lines.addAll(generateEmptyLengthAssertions());
            lines.addAll(generateSubsetFunctions());

            return lines;
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
        }

        /**
Solution content 
         * {@inheritDoc}
         */
        @Override
        public List generateInitialisers() {
            List initialisers = new ArrayList<>();

            initialisers.addAll(generateSorts());
            initialisers.addAll(generateAddFunctions());
            initialisers.addAll(generateContainsFunctions());
            initialisers.addAll(generateRemoveFunctions());
            initialisers.addAll(generateEmptyConstants());
            initialisers.addAll(generateLengthFunctions());
            initialisers.addAll(generateEmptyLengthAssertions());
            initialisers.addAll(generateSubsetFunctions());
            // Causes lots of the tests to timeout
            //            initialisers.addAll(generateSubsetLengthAssertions());

            return initialisers;
        }

        /**
File
Sort.java
Developer's decision
Version 1
Kind of conflict
Comment
Method invocation
Method signature
Return statement
Variable
Chunk
Conflicting content 
            return "(" + getName() + " " + type + ")";
        }

<<<<<<< HEAD
        private List generateAddFunctions() {
            List> parameters = new ArrayList<>();
            parameters.add(new Pair<>("set", toString()));
            parameters.add(new Pair<>("t", type));
=======
        private List generateAddFunctions() {
            List> parameters = new ArrayList>();
            parameters.add(new Pair("set", toString()));
            parameters.add(new Pair("t", type));
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
            String expr = "(store set t true)";

            return Arrays.asList(new Stmt.DefineFun(FUN_ADD_NAME, parameters, toString(),
Solution content 
            return "(" + getName() + " " + type + ")";
        }

        private List generateAddFunctions() {
            List> parameters = new ArrayList<>();
            parameters.add(new Pair<>("set", toString()));
            parameters.add(new Pair<>("t", type));
            String expr = "(store set t true)";

            return Arrays.asList(new Stmt.DefineFun(FUN_ADD_NAME, parameters, toString(),
File
Sort.java
Developer's decision
Version 1
Kind of conflict
Method invocation
Method signature
Variable
Chunk
Conflicting content 
                    expr));
        }

<<<<<<< HEAD
        private List generateContainsFunctions() {
            List> parameters = new ArrayList<>();
            parameters.add(new Pair<>("set", toString()));
            parameters.add(new Pair<>("t", type));
=======
        private List generateContainsFunctions() {
            List> parameters = new ArrayList>();
            parameters.add(new Pair("set", toString()));
            parameters.add(new Pair("t", type));
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
            String expr = "(select set t)";

            return Arrays.asList(new Stmt.DefineFun(FUN_CONTAINS_NAME, parameters, BOOL,
Solution content 
                    expr));
        }

        private List generateContainsFunctions() {
            List> parameters = new ArrayList<>();
            parameters.add(new Pair<>("set", toString()));
            parameters.add(new Pair<>("t", type));
            String expr = "(select set t)";

            return Arrays.asList(new Stmt.DefineFun(FUN_CONTAINS_NAME, parameters, BOOL,
File
Sort.java
Developer's decision
Version 1
Kind of conflict
Method invocation
Method signature
Variable
Chunk
Conflicting content 
                    expr));
        }

<<<<<<< HEAD
        private List generateEmptyConstants() {
            List stmts = new ArrayList<>();
=======
        private List generateEmptyConstants() {
            List lines = new ArrayList();
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123

            stmts.add(new Stmt.DeclareFun(FUN_EMPTY_NAME, Collections.EMPTY_LIST, toString()));
            // The empty set does not contain any elements
Solution content 
                    expr));
        }

        private List generateEmptyConstants() {
            List stmts = new ArrayList<>();

            stmts.add(new Stmt.DeclareFun(FUN_EMPTY_NAME, Collections.EMPTY_LIST, toString()));
            // The empty set does not contain any elements
File
Sort.java
Developer's decision
Version 1
Kind of conflict
Method invocation
Method signature
Variable
Chunk
Conflicting content 
            return stmts;
        }

<<<<<<< HEAD
        private List generateEmptyLengthAssertions() {
            return Arrays.asList(new Stmt.Assert("(= (length " + FUN_EMPTY_NAME + ") 0)"));
        }

        private List generateLengthFunctions() {
            List stmts = new ArrayList<>();

            stmts.add(new Stmt.DeclareFun(FUN_LENGTH_NAME, Arrays.asList(toString()), INT));
            // The length of all sets is a natural number
            stmts.add(new Stmt.Assert("(forall ((set " + toString() + ")) (<= 0 (length set)))"));
            // A recursive conjecture for determining the length of sets
            // Either a set is empty (and hence its length is 0) or:
            // There exists some element t, contained within the set, hence its length must be 1 +
            // the length of the set minus t
            stmts.add(new Stmt.Assert(
                    "(forall ((set " + toString() + ")) (=> (not (= set " + FUN_EMPTY_NAME
                            + ")) (exists ((t " + type
=======
        private List generateEmptyLengthAssertions() {
            List lines = new ArrayList();

            lines.add(new Stmt.Assert("(= (length empty) 0)"));

            return lines;
        }

        private List generateInitialisors() {
            List parameters = Arrays.asList("T");
            String expr = "(" + ARRAY + " T " + BOOL + ")";

            return Arrays.asList(new Stmt.DefineSort(getName(), parameters, expr));
        }

        private List generateLengthFunctions() {
            List lines = new ArrayList();

            lines.add(new Stmt.DeclareFun(FUN_LENGTH_NAME, Arrays.asList(toString()), INT));
            lines.add(new Stmt.Assert("(forall ((set " + toString() + ")) (<= 0 (length set)))"));
            //            TODO: Make this IFF not implication
            lines.add(new Stmt.Assert(
                    "(forall ((set " + toString() + ")) (=> (not (= set empty)) (exists ((t " + type
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
                            + ")) (and (contains set t) (= (length set) (+ 1 (length (remove set t))))))))"));
            // TODO: This conjecture really should be iff or xor (going both ways), however using
            // xor causes it to time out, so for now we use implication
Solution content 
            return stmts;
        }

        private List generateEmptyLengthAssertions() {
            return Arrays.asList(new Stmt.Assert("(= (length " + FUN_EMPTY_NAME + ") 0)"));
        }

        private List generateLengthFunctions() {
            List stmts = new ArrayList<>();

            stmts.add(new Stmt.DeclareFun(FUN_LENGTH_NAME, Arrays.asList(toString()), INT));
            // The length of all sets is a natural number
            stmts.add(new Stmt.Assert("(forall ((set " + toString() + ")) (<= 0 (length set)))"));
            // A recursive conjecture for determining the length of sets
            // Either a set is empty (and hence its length is 0) or:
            // There exists some element t, contained within the set, hence its length must be 1 +
            // the length of the set minus t
            stmts.add(new Stmt.Assert(
                    "(forall ((set " + toString() + ")) (=> (not (= set " + FUN_EMPTY_NAME
                            + ")) (exists ((t " + type
                            + ")) (and (contains set t) (= (length set) (+ 1 (length (remove set t))))))))"));
            // TODO: This conjecture really should be iff or xor (going both ways), however using
            // xor causes it to time out, so for now we use implication
File
Sort.java
Developer's decision
Version 1
Kind of conflict
Comment
Method declaration
Method invocation
Method signature
Variable
Chunk
Conflicting content 
            return stmts;
        }

<<<<<<< HEAD
        private List generateRemoveFunctions() {
            List> parameters = new ArrayList<>();
            parameters.add(new Pair<>("set", toString()));
            parameters.add(new Pair<>("t", type));
=======
        private List generateRemoveFunctions() {
            List> parameters = new ArrayList>();
            parameters.add(new Pair("set", toString()));
            parameters.add(new Pair("t", type));
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
            String expr = "(store set t false)";

            return Arrays.asList(new Stmt.DefineFun(FUN_REMOVE_NAME, parameters, toString(),
Solution content 
            return stmts;
        }

        private List generateRemoveFunctions() {
            List> parameters = new ArrayList<>();
            parameters.add(new Pair<>("set", toString()));
            parameters.add(new Pair<>("t", type));
            String expr = "(store set t false)";

            return Arrays.asList(new Stmt.DefineFun(FUN_REMOVE_NAME, parameters, toString(),
File
Sort.java
Developer's decision
Version 1
Kind of conflict
Method invocation
Method signature
Variable
Chunk
Conflicting content 
                    expr));
        }

<<<<<<< HEAD
        private List generateSorts() {
            List parameters = Arrays.asList("T");
            String expr = "(" + ARRAY + " T " + BOOL + ")";

            return Arrays.asList(new Stmt.DefineSort(getName(), parameters, expr));
        }

        private List generateSubsetFunctions() {
            List> parameters = new ArrayList<>();
            parameters.add(new Pair<>("first", toString()));
            parameters.add(new Pair<>("second", toString()));
=======
        private List generateSubsetFunctions() {
            List> parameters = new ArrayList>();
            parameters.add(new Pair("first", toString()));
            parameters.add(new Pair("second", toString()));
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
            String subseteqExpr =
                    "(forall ((t " + type + ")) (=> (contains first t) (contains second t)))";
            String subsetExpr = "(and (subseteq first second) (exists ((t " + type
Solution content 
                    expr));
        }

        private List generateSorts() {
            List parameters = Arrays.asList("T");
            String expr = "(" + ARRAY + " T " + BOOL + ")";

            return Arrays.asList(new Stmt.DefineSort(getName(), parameters, expr));
        }

        private List generateSubsetFunctions() {
            List> parameters = new ArrayList<>();
            parameters.add(new Pair<>("first", toString()));
            parameters.add(new Pair<>("second", toString()));
            String subseteqExpr =
                    "(forall ((t " + type + ")) (=> (contains first t) (contains second t)))";
            String subsetExpr = "(and (subseteq first second) (exists ((t " + type
File
Sort.java
Developer's decision
Version 1
Kind of conflict
Method declaration
Method invocation
Method signature
Variable
Chunk
Conflicting content 
            // Alternative that uses the length function
            // String subsetExpr = "(and (subseteq first second) (distinct (length first) (length second)))";

<<<<<<< HEAD
            List functions = new ArrayList<>();
=======
            List functions = new ArrayList();
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
            functions.add(new Stmt.DefineFun(FUN_SUBSETEQ_NAME, parameters, BOOL, subseteqExpr));
            functions.add(new Stmt.DefineFun(FUN_SUBSET_NAME, parameters, BOOL, subsetExpr));
Solution content 
            // Alternative that uses the length function
            // String subsetExpr = "(and (subseteq first second) (distinct (length first) (length second)))";

            List functions = new ArrayList<>();
            functions.add(new Stmt.DefineFun(FUN_SUBSETEQ_NAME, parameters, BOOL, subseteqExpr));
            functions.add(new Stmt.DefineFun(FUN_SUBSET_NAME, parameters, BOOL, subsetExpr));
File
Sort.java
Developer's decision
Version 1
Kind of conflict
Method invocation
Variable
Chunk
Conflicting content 
                throw new NullPointerException("types cannot contain null");
            }

<<<<<<< HEAD
            this.types = Collections.unmodifiableList(new ArrayList<>(types));
=======
            this.types = new ArrayList(types);
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
        }

        public static String generateGetFunctionName(int index) {
Solution content 
                throw new NullPointerException("types cannot contain null");
            }

            this.types = Collections.unmodifiableList(new ArrayList<>(types));
        }

        public static String generateGetFunctionName(int index) {
File
Sort.java
Developer's decision
Version 1
Kind of conflict
Attribute
Method invocation
Chunk
Conflicting content 
         * {@inheritDoc}
         */
        @Override
<<<<<<< HEAD
        public List generateInitialisers() {
            List initialisers = new ArrayList<>();
=======
        public List generateLines() {
            List lines = new ArrayList();
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123

            initialisers.addAll(generateSorts());
            initialisers.addAll(generateGetFunctions());
Solution content 
         * {@inheritDoc}
         */
        @Override
        public List generateInitialisers() {
            List initialisers = new ArrayList<>();

            initialisers.addAll(generateSorts());
            initialisers.addAll(generateGetFunctions());
File
Sort.java
Developer's decision
Version 1
Kind of conflict
Method invocation
Method signature
Variable
Chunk
Conflicting content 
            return sb.toString();
        }

<<<<<<< HEAD
        private List generateEqualityAssertions() {
            List stmts = new ArrayList<>();

            // Two tuples are equal if and only if all of their elements are equal
            StringBuilder premise = new StringBuilder("(and");
            for (int i = 0; i < types.size(); i++) {
                premise.append(" (= ");
                premise.append("(");
                premise.append(generateGetFunctionName(i));
                premise.append(" tuple0");
                premise.append(")");
                premise.append("(");
                premise.append(generateGetFunctionName(i));
                premise.append(" tuple1");
                premise.append(")");
                premise.append(")");
            }
            premise.append(")");
            stmts.add(new Stmt.Assert(
                    "(forall ((tuple0 " + toString() + ") (tuple1 " + toString() + ")) (xor "
                            + premise + " (distinct tuple0 tuple1)))"));

            return stmts;
        }

        private List generateGetFunctions() {
            List stmts = new ArrayList<>();
=======
        private List generateGetFunctions() {
            List getFunctions = new ArrayList();
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123

            for (int i = 0; i < types.size(); i++) {
                stmts.add(new Stmt.DeclareFun(generateGetFunctionName(i), Arrays.asList(toString()),
Solution content 
            return sb.toString();
        }

        private List generateEqualityAssertions() {
            List stmts = new ArrayList<>();

            // Two tuples are equal if and only if all of their elements are equal
            StringBuilder premise = new StringBuilder("(and");
            for (int i = 0; i < types.size(); i++) {
                premise.append(" (= ");
                premise.append("(");
                premise.append(generateGetFunctionName(i));
                premise.append(" tuple0");
                premise.append(")");
                premise.append("(");
                premise.append(generateGetFunctionName(i));
                premise.append(" tuple1");
                premise.append(")");
                premise.append(")");
            }
            premise.append(")");
            stmts.add(new Stmt.Assert(
                    "(forall ((tuple0 " + toString() + ") (tuple1 " + toString() + ")) (xor "
                            + premise + " (distinct tuple0 tuple1)))"));

            return stmts;
        }

        private List generateGetFunctions() {
            List stmts = new ArrayList<>();

            for (int i = 0; i < types.size(); i++) {
                stmts.add(new Stmt.DeclareFun(generateGetFunctionName(i), Arrays.asList(toString()),
File
Sort.java
Developer's decision
Version 1
Kind of conflict
Method declaration
Method invocation
Method signature
Variable
Chunk
Conflicting content 
            this.name = name;
            this.returnSort = returnSort;
<<<<<<< HEAD
            this.parameterSorts = Collections.unmodifiableList(new ArrayList<>(parameterSorts));
=======
            this.parameterSorts = new ArrayList(parameterSorts);
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
        }

        /**
Solution content 
            this.name = name;
            this.returnSort = returnSort;
            this.parameterSorts = Collections.unmodifiableList(new ArrayList<>(parameterSorts));
        }

        /**
File
Stmt.java
Developer's decision
Version 1
Kind of conflict
Attribute
Method invocation
Chunk
Conflicting content 
            this.name = name;
            this.returnSort = returnSort;
<<<<<<< HEAD
            this.parameters = Collections.unmodifiableList(new ArrayList<>(parameters));
=======
            this.parameters = new ArrayList>(parameters);
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
            this.expr = expr;
        }
Solution content 
            this.name = name;
            this.returnSort = returnSort;
            this.parameters = Collections.unmodifiableList(new ArrayList<>(parameters));
            this.expr = expr;
        }
File
Stmt.java
Developer's decision
Version 1
Kind of conflict
Attribute
Method invocation
Chunk
Conflicting content 
            }

            this.name = name;
<<<<<<< HEAD
            this.parameters = Collections.unmodifiableList(new ArrayList<>(parameters));
=======
            this.parameters = new ArrayList(parameters);
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
            this.expr = expr;
        }
Solution content 
            }

            this.name = name;
            this.parameters = Collections.unmodifiableList(new ArrayList<>(parameters));
            this.expr = expr;
        }
File
Stmt.java
Developer's decision
Version 1
Kind of conflict
Attribute
Method invocation
Chunk
Conflicting content 
        // Recursion potential here! Skip if we've already generated the declaration and assertion

<<<<<<< HEAD
        // A function can be uniquely identified by it's identifier and generic binding
        if (!functions.contains(new Pair<>(id, generics))) {
            functions.add(new Pair<>(id, generics));

            // Generate the uninterpreted function declaration

            List parameters = new ArrayList<>();
=======
        // A function can be uniquely identified by it's name and generic binding
        if (!functions.contains(new Pair(function.name(), generics))) {
            functions.add(new Pair(function.name(), generics));

            // Generate the uninterpreted function declaration

            String name = code.nid.name();
            List parameters = new ArrayList();
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
            parameters.add(translate(type.from()));
            String returnSort = translate(type.to());
Solution content 
        // Recursion potential here! Skip if we've already generated the declaration and assertion

        // A function can be uniquely identified by it's identifier and generic binding
        if (!functions.contains(new Pair<>(id, generics))) {
            functions.add(new Pair<>(id, generics));

            // Generate the uninterpreted function declaration

            List parameters = new ArrayList<>();
            parameters.add(translate(type.from()));
            String returnSort = translate(type.to());
File
SmtVerificationCheck.java
Developer's decision
Version 1
Kind of conflict
Comment
If statement
Method invocation
Variable
Chunk
Conflicting content 
        if (!(code instanceof Code.Quantifier)) {
            // Guess not, let's negate it and check for UNSAT anyway as UNSAT is easier for a solver
            // to determine (and lets our length function work properly)
<<<<<<< HEAD
            return new Pair<>("(not " + translate(code) + ")", Response.UNSAT);
=======
            return new Pair("(not " + translate(code) + ")", Result.UNSAT);
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
        }

        Code.Quantifier quantifier = (Code.Quantifier) code;
Solution content 
        if (!(code instanceof Code.Quantifier)) {
            // Guess not, let's negate it and check for UNSAT anyway as UNSAT is easier for a solver
            // to determine (and lets our length function work properly)
            return new Pair<>("(not " + translate(code) + ")", Response.UNSAT);
        }

        Code.Quantifier quantifier = (Code.Quantifier) code;
File
SmtVerificationCheck.java
Developer's decision
Version 1
Kind of conflict
Method invocation
Return statement
Chunk
Conflicting content 
        // declare-sort x
        // assert a and b and c
        if (code.opcode == Code.Op.EXISTS) {
<<<<<<< HEAD
            return new Pair<>(translate(operand), Response.SAT);
=======
            return new Pair(translate(operand), Result.SAT);
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
        }

        // Opcode must be a FORALL
Solution content 
        // declare-sort x
        // assert a and b and c
        if (code.opcode == Code.Op.EXISTS) {
            return new Pair<>(translate(operand), Response.SAT);
        }

        // Opcode must be a FORALL
File
SmtVerificationCheck.java
Developer's decision
Version 1
Kind of conflict
Method invocation
Return statement
Chunk
Conflicting content 
        // If it doesn't happen to be an OR, then we can still translate it treating it as if it
        // were an or of a single term
        if (operand.opcode != Code.Op.OR) {
<<<<<<< HEAD
            return new Pair<>("(not " + translate(operand) + ")", Response.UNSAT);
=======
            return new Pair("(not " + translate(operand) + ")", Result.UNSAT);
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
        }

        // Looks like the FORALL is over an OR (or implication), got to add the negated premises
Solution content 
        // If it doesn't happen to be an OR, then we can still translate it treating it as if it
        // were an or of a single term
        if (operand.opcode != Code.Op.OR) {
            return new Pair<>("(not " + translate(operand) + ")", Response.UNSAT);
        }

        // Looks like the FORALL is over an OR (or implication), got to add the negated premises
File
SmtVerificationCheck.java
Developer's decision
Version 1
Kind of conflict
Method invocation
Return statement
Chunk
Conflicting content 
        String expr = translate(operand.operands[operand.operands.length - 1]);
        expr = "(not " + expr + ")";

<<<<<<< HEAD
        return new Pair<>(expr, Response.UNSAT);
=======
        return new Pair(expr, Result.UNSAT);
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
    }

    private String translateSet(Code.Nary code) {
Solution content 
        String expr = translate(operand.operands[operand.operands.length - 1]);
        expr = "(not " + expr + ")";

        return new Pair<>(expr, Response.UNSAT);
    }

    private String translateSet(Code.Nary code) {
File
SmtVerificationCheck.java
Developer's decision
Version 1
Kind of conflict
Method invocation
Return statement
Chunk
Conflicting content 
    private File write() throws IOException {
        // Prepare the output destination
        File out = File.createTempFile("wycs_" + wycsFile.id() + "_", ".smt2");
<<<<<<< HEAD
=======
        if (!out.exists()) {
            throw new IOException("unable to create temp file: " + smt2File);
        }
>>>>>>> 42fbb6029086e408635853543bd4a125b28b8123
        if (!DEBUG) {
            out.deleteOnExit();
        }
Solution content 
    private File write() throws IOException {
        // Prepare the output destination
        File out = File.createTempFile("wycs_" + wycsFile.id() + "_", ".smt2");
        if (!DEBUG) {
            out.deleteOnExit();
        }
File
SmtVerificationCheck.java
Developer's decision
Version 1
Kind of conflict
If statement