mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-05 19:00:33 -05:00
15 lines
565 B
Text
15 lines
565 B
Text
(set-info :smt-lib-version 2.6)
|
|
(set-logic QF_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 :category "industrial")
|
|
(set-info :status sat)
|
|
(declare-sort S1 0)
|
|
(declare-fun f1 () S1)
|
|
(declare-fun f2 () S1)
|
|
(declare-fun f3 (Real) Real)
|
|
(declare-fun f4 () Real)
|
|
(declare-fun f5 () Real)
|
|
(assert (not (= f1 f2)))
|
|
(assert (not (= (f3 (- f4 f5)) (- (f3 f4)))))
|
|
(check-sat)
|
|
(exit)
|