summaryrefslogtreecommitdiff
path: root/Binaries/UnivBackPred2.smt2
blob: d3e3777ffef211a25bb5ad9e51e683d743e14379 (plain)
1
2
3
4
5
6
7
8
9
; 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 int_div (Int Int) Int)
(declare-fun int_mod (Int Int) Int)
(declare-fun UOrdering2 (|T@U| |T@U|) Bool)
(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)