Solver Disagreements on QF_SLIA (Single Query Track)

Page generated on 2020-07-02 15:49:34 +0000

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-addStrings/397.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-addStrings/463.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/103.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/107.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/115.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/152.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/179.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/18.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/191.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/207.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/260.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/272.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/290.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/294.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/3.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/304.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/309.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/327.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/359.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/363.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/401.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/498.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/508.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/622.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/644.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/666.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/690.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/696.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/8.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/89.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_cvc4/leetcode_int-add_binary/93.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-addStrings/995.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/110.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/111.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/113.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/114.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/121.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/141.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/157.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/158.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/172.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/203.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/77.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/90.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-add_binary/1102.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-add_binary/290.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-add_binary/344.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-add_binary/350.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-add_binary/502.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-add_binary/652.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-add_binary/726.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-add_binary/736.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-add_binary/776.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-add_binary/782.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-add_binary/896.smt2

• Z3str4: sat
• CVC4: unsat

QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-add_binary/970.smt2

• Z3str4: sat
• CVC4: unsat

ⁿ Non-competing.
^u Solver is unsound in this division.