Commit a3173345 authored by Clark Barrett's avatar Clark Barrett
Browse files

Squashed commit of the following:

commit 4597f0d0
Author: Pascal Fontaine <Pascal.Fontaine@loria.fr>
Date:   Mon Jun 5 18:00:39 2017 +0200

    Fixing README.md

commit a86b9481
Author: Pascal Fontaine <Pascal.Fontaine@loria.fr>
Date:   Mon Jun 5 16:55:38 2017 +0200

    Fixing README.md

commit 7f0b396d
Author: Pascal Fontaine <Pascal.Fontaine@loria.fr>
Date:   Tue May 23 14:46:20 2017 +0200

    2.0 to 2.6, CRLF to LF

commit 5a2add48
Author: Pascal Fontaine <Pascal.Fontaine@inria.fr>
Date:   Wed May 3 18:23:53 2017 +0200

    Fixing README.md

commit c4901056
Author: Pascal Fontaine <Pascal.Fontaine@inria.fr>
Date:   Thu Apr 20 10:11:48 2017 +0200

    Fixing README.md

commit fc903093
Author: Pascal Fontaine <Pascal.Fontaine@inria.fr>
Date:   Wed Mar 29 13:47:32 2017 +0200

    Fixing README.md

commit e5df3f08
Author: Pascal Fontaine <Pascal.Fontaine@loria.fr>
Date:   Tue Mar 28 16:36:15 2017 +0200

    Fixing README.md

commit 2619a202
Author: Tjark Weber <tjark.weber@gmx.de>
Date:   Thu Mar 16 10:32:04 2017 +0100

    Remove duplicate benchmarks
parent ffbe7f2a
(set-info :smt-lib-version 2.6)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
......
(set-info :smt-lib-version 2.6)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
......
(set-info :smt-lib-version 2.6)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
......
(set-info :smt-lib-version 2.6)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
......
(set-info :smt-lib-version 2.6)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
......
(set-info :smt-lib-version 2.6)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
......
(set-info :smt-lib-version 2.6)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
......
(set-info :smt-lib-version 2.6)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
......
(set-info :smt-lib-version 2.6)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
......
(set-info :smt-lib-version 2.6)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
......
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (= (f3 f4 (- f5 f6)) (- (f3 f4 f5)))))
(assert (forall ((?v0 Real)) (= (f3 f4 (+ f6 ?v0)) (- (f3 f4 ?v0)))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (forall ((?v0 Real)) (= (f3 f4 (+ f5 ?v0)) (- (f3 f4 ?v0)))))
(assert (not (= (f3 f4 (- f6 f5)) (- (f3 f4 f6)))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (not (= (f3 f4 f5) 0.0))))
(assert (< 0.0 f5))
(assert (< f5 f6))
(assert (< 0.0 f5))
(assert (< f5 f6))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f6) (< ?v_0 (f3 f4 ?v0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (not (= (f3 f4 f5) 0.0))))
(assert (< 0.0 f5))
(assert (< f5 f6))
(assert (< f5 f6))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f6) (< ?v_0 (f3 f4 ?v0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (not (= (f3 f4 f5) 0.0))))
(assert (< 0.0 f5))
(assert (< f5 f6))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f6) (< ?v_0 (f3 f4 ?v0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 () Real)
(declare-fun f4 (S2 Real) Real)
(declare-fun f5 () S2)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f3) (< ?v_0 (f4 f5 ?v0)))))))
(assert (let ((?v_0 0.0)) (not (=> (< ?v_0 f6) (=> (< f6 f3) (not (= (f4 f5 f6) ?v_0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (not (= (f3 f4 (- f5 f6)) 0.0))))
(assert (< 0.0 (- f5 f6)))
(assert (< (- f5 f6) f6))
(assert (< 0.0 (- f5 f6)))
(assert (< (- f5 f6) f6))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f6) (< ?v_0 (f3 f4 ?v0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (not (= (f3 f4 (- f5 f6)) 0.0))))
(assert (< 0.0 (- f5 f6)))
(assert (< (- f5 f6) f6))
(assert (< (- f5 f6) f6))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f6) (< ?v_0 (f3 f4 ?v0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 Real) Real)
(declare-fun f4 () S2)
(declare-fun f5 () Real)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (not (not (= (f3 f4 (- f5 f6)) 0.0))))
(assert (< 0.0 (- f5 f6)))
(assert (< (- f5 f6) f6))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f6) (< ?v_0 (f3 f4 ?v0)))))))
(check-sat)
(exit)
(set-logic UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 () Real)
(declare-fun f4 (S2 Real) Real)
(declare-fun f5 () S2)
(declare-fun f6 () Real)
(assert (not (= f1 f2)))
(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (< ?v_0 ?v0) (=> (< ?v0 f3) (< ?v_0 (f4 f5 ?v0)))))))
(assert (let ((?v_1 0.0) (?v_0 (- f6 f3))) (not (=> (< ?v_1 ?v_0) (=> (< ?v_0 f3) (not (= (f4 f5 ?v_0) ?v_1)))))))
(check-sat)
(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