summaryrefslogtreecommitdiff
path: root/Binaries/UnivBackPred2.smt2
blob: 9bb05bfb615eeede49354b37a8bec5b7d004225e (plain)
1
2
3
4
5
6
7
8
; Boogie universal background predicate
; Copyright (c) 2004-2010, Microsoft Corp.
(set-info :category "industrial")
(declare-sort |T@U| 0)
(declare-sort |T@T| 0)
(declare-fun real_pow (Real Real) Real)
(declare-fun UOrdering2 (|T@U| |T@U|) Bool)
(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)