Commit 03ddbd11 authored by Tjark Weber's avatar Tjark Weber
Browse files

Remove duplicate benchmarks

parent d4ce2379
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(define-fun _2 () Bool false)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment