diff options
| author |  MichalMoskal <unknown> | 2011-02-17 19:00:30 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-17 19:00:30 +0000 |
| commit | 6b85a0f0d4f88b6ad57812175354acf3a2947a0e (patch) | |
| tree | c214ed7a953471eaf2689a6b7517cd0ead5fb9bf /Binaries | |
| parent | 12027267b93833110c0a1a044e1bc80ebf6e7b29 (diff) | |
Provide /p: as the short form of /proverOpt:.
Add /p:O:<name>=<value> and /p:C:<solver-argument> prover options in SMT.
Add default Z3 options when using Z3.
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/UnivBackPred2.smt2 | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2 index 4490d2cb..ee553a98 100644 --- a/Binaries/UnivBackPred2.smt2 +++ b/Binaries/UnivBackPred2.smt2 @@ -1,9 +1,7 @@ ; Boogie universal background predicate
; Copyright (c) 2004-2010, Microsoft Corp.
-
-(set-logic UFNIA)
-(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
+(set-logic UFNIA)
(declare-sort |T@U| 0)
(declare-sort |T@T| 0)
(declare-fun int_div (Int Int) Int)
|