diff options
author | 2011-05-10 08:17:51 -0700 | |
---|---|---|
committer | 2011-05-10 08:17:51 -0700 | |
commit | 633a8917f18fa66a0eda659899cf8cbe18634330 (patch) | |
tree | 8ec63c644685424287d10383ef4aa033557def4a | |
parent | eb8e52a4e8fb049d83c7143da3110a8ec2740474 (diff) | |
parent | 0016df228b3a12fdf68e48f05b41bb7621990c3b (diff) |
Merge
-rw-r--r-- | Binaries/UnivBackPred2.smt2 | 1 | ||||
-rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 7 |
2 files changed, 7 insertions, 1 deletions
diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2 index 06b307fe..97c052c9 100644 --- a/Binaries/UnivBackPred2.smt2 +++ b/Binaries/UnivBackPred2.smt2 @@ -1,7 +1,6 @@ ; Boogie universal background predicate
; Copyright (c) 2004-2010, Microsoft Corp.
(set-info :category "industrial")
-(set-logic UFNIA)
(declare-sort |T@U| 0)
(declare-sort |T@T| 0)
(declare-fun int_div (Int Int) Int)
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 7b4d170d..42cf89ab 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -151,6 +151,13 @@ namespace Microsoft.Boogie.SMTLib foreach (var opt in options.SmtOptions) {
SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");
}
+
+ if (CommandLineOptions.Clo.UseArrayTheory) {
+ SendCommon("; skipping logic setting (using arrays)");
+ } else {
+ SendCommon("(set-logic UFNIA)");
+ }
+
SendCommon("; done setting options\n");
SendCommon(_backgroundPredicates);
}
|