summaryrefslogtreecommitdiff
path: root/Binaries/UnivBackPred2.smt2
blob: 1cfe53562562399a533e536bb1c1e747641d5cfe (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
; -------------------------------------------------------------------------
; Boogie universal background predicate
; Copyright (c) 2004-2010, Microsoft Corp.

(set-logic UFNIA)
(set-info :smt-lib-version 2.0)
(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)