Solver Disagreements on UF (Incremental Track)

Page generated on 2020-07-02 17:01:54 +0000

UF/20190906-CLEARSY/0000/00302.smt2 query 2

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00302.smt2 query 3

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00302.smt2 query 4

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00307.smt2 query 2

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00307.smt2 query 3

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00307.smt2 query 8

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00307.smt2 query 9

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00307.smt2 query 10

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00307.smt2 query 11

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00307.smt2 query 14

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00307.smt2 query 21

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00307.smt2 query 22

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00307.smt2 query 23

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00307.smt2 query 24

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00307.smt2 query 25

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0000/00307.smt2 query 26

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00001.smt2 query 33

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00001.smt2 query 47

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00001.smt2 query 51

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00001.smt2 query 60

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00077.smt2 query 10

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00097.smt2 query 6

• z3ⁿ: sat
• SMTInterpol: unsat

UF/20190906-CLEARSY/0001/00104.smt2 query 12

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00172.smt2 query 5

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00172.smt2 query 8

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00172.smt2 query 9

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00172.smt2 query 10

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00288.smt2 query 21

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00288.smt2 query 23

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00288.smt2 query 24

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00288.smt2 query 25

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00310.smt2 query 33

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00310.smt2 query 34

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00310.smt2 query 39

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00310.smt2 query 40

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00310.smt2 query 41

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00310.smt2 query 42

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00310.smt2 query 45

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00310.smt2 query 52

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00310.smt2 query 53

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00310.smt2 query 54

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00310.smt2 query 55

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00310.smt2 query 56

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0001/00310.smt2 query 57

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0008/00017.smt2 query 7

• SMTInterpol-fixedⁿ: sat
• CVC4-inc: sat
• z3ⁿ: sat
• SMTInterpol: unsat

UF/20190906-CLEARSY/0008/00017.smt2 query 8

• SMTInterpol-fixedⁿ: sat
• CVC4-inc: sat
• z3ⁿ: sat
• SMTInterpol: unsat

UF/20190906-CLEARSY/0008/00017.smt2 query 9

• SMTInterpol-fixedⁿ: sat
• CVC4-inc: sat
• z3ⁿ: sat
• SMTInterpol: unsat

UF/20190906-CLEARSY/0008/00017.smt2 query 10

• SMTInterpol-fixedⁿ: sat
• CVC4-inc: sat
• z3ⁿ: sat
• SMTInterpol: unsat

UF/20190906-CLEARSY/0008/00017.smt2 query 11

• SMTInterpol-fixedⁿ: sat
• CVC4-inc: sat
• z3ⁿ: sat
• SMTInterpol: unsat

UF/20190906-CLEARSY/0012/00009.smt2 query 100

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0012/00092.smt2 query 30

• SMTInterpol-fixedⁿ: sat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0015/00015.smt2 query 71

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0015/00019.smt2 query 105

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0015/00116.smt2 query 20

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0015/00116.smt2 query 21

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0015/00206.smt2 query 50

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0015/00210.smt2 query 24

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0015/00210.smt2 query 29

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00042.smt2 query 71

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00053.smt2 query 41

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00434.smt2 query 38

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00442.smt2 query 2

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00442.smt2 query 4

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00442.smt2 query 6

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00442.smt2 query 8

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00442.smt2 query 10

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00442.smt2 query 12

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00442.smt2 query 14

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00461.smt2 query 11

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00461.smt2 query 16

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00466.smt2 query 9

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00466.smt2 query 26

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00568.smt2 query 41

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00600.smt2 query 45

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00688.smt2 query 17

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0016/00693.smt2 query 41

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0017/00003.smt2 query 10

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0020/00012.smt2 query 25

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0021/00019.smt2 query 60

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0021/00019.smt2 query 74

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0021/00019.smt2 query 88

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0021/00019.smt2 query 96

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0021/00019.smt2 query 104

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0021/00019.smt2 query 113

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0021/00019.smt2 query 120

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0022/00004.smt2 query 14

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0022/00004.smt2 query 15

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0022/00004.smt2 query 21

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0023/00245.smt2 query 12

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0023/00245.smt2 query 13

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0023/00245.smt2 query 14

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0023/00245.smt2 query 15

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0023/00245.smt2 query 16

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0023/00245.smt2 query 17

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0023/00245.smt2 query 23

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0023/00245.smt2 query 24

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

UF/20190906-CLEARSY/0024/00342.smt2 query 8

• SMTInterpol-fixedⁿ: unsat
• CVC4-inc: unsat
• z3ⁿ: unsat
• SMTInterpol: sat

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