Merge pull request #13 from aronspang/main

Added QF_LIA Benchmarks
SMT-LIB · Apr 13, 2024 · 2f460b2 · 2f460b2
2 parents 080d116 + 4bfcd8d
commit 2f460b2
Show file tree

Hide file tree

Showing 80 changed files with 3,330,501 additions and 0 deletions.
diff --git a/non-incremental/QF_LIA/20231117-c_inference/100_100_20_11_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/100_100_20_11_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/100_100_20_12_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/100_100_20_12_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/100_100_20_16_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/100_100_20_16_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/100_100_20_1_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/100_100_20_1_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/100_100_20_6_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/100_100_20_6_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/100_100_36_15_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/100_100_36_15_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/100_100_47_17_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/100_100_47_17_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/100_100_47_5_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/100_100_47_5_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/100_100_78_15_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/100_100_78_15_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/100_100_89_19_unsat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/100_100_89_19_unsat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/30_30_18_12_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/30_30_18_12_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/30_30_18_15_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/30_30_18_15_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/30_30_18_1_unsat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/30_30_18_1_unsat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/30_30_18_20_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/30_30_18_20_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/30_30_18_2_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/30_30_18_2_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/30_30_18_3_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/30_30_18_3_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/30_30_18_5_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/30_30_18_5_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/30_30_18_8_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/30_30_18_8_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/30_30_82_6_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/30_30_82_6_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/30_30_86_7_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/30_30_86_7_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/40_40_11_12_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/40_40_11_12_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/40_40_11_3_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/40_40_11_3_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/40_40_11_5_unsat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/40_40_11_5_unsat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/40_40_11_7_unsat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/40_40_11_7_unsat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/40_40_15_9_unsat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/40_40_15_9_unsat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/40_40_58_4_unsat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/40_40_58_4_unsat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/40_40_78_12_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/40_40_78_12_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/40_40_78_14_unsat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/40_40_78_14_unsat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/40_40_78_15_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/40_40_78_15_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/40_40_78_5_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/40_40_78_5_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/50_50_12_10_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/50_50_12_10_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/50_50_12_14_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/50_50_12_14_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/50_50_45_12_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/50_50_45_12_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/50_50_45_4_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/50_50_45_4_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/50_50_45_6_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/50_50_45_6_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/50_50_53_1_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/50_50_53_1_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/50_50_74_13_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/50_50_74_13_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/50_50_74_6_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/50_50_74_6_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/50_50_80_12_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/50_50_80_12_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/50_50_81_19_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/50_50_81_19_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/60_60_46_15_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/60_60_46_15_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/60_60_46_17_unsat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/60_60_46_17_unsat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/60_60_46_1_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/60_60_46_1_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/60_60_46_20_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/60_60_46_20_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/60_60_46_4_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/60_60_46_4_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/60_60_8_2_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/60_60_8_2_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/60_60_90_13_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/60_60_90_13_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/60_60_90_15_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/60_60_90_15_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/60_60_90_17_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/60_60_90_17_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/60_60_90_20_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/60_60_90_20_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/70_70_68_13_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/70_70_68_13_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/70_70_68_2_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/70_70_68_2_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/70_70_68_7_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/70_70_68_7_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/70_70_6_4_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/70_70_6_4_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/70_70_80_13_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/70_70_80_13_sat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/70_70_80_2_unsat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/70_70_80_2_unsat.smt2
diff --git a/non-incremental/QF_LIA/20231117-c_inference/70_70_96_12_sat.smt2 b/non-incremental/QF_LIA/20231117-c_inference/70_70_96_12_sat.smt2