diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-05-09 17:22:52 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-05-09 17:22:52 -0700 |
| commit | 0016df228b3a12fdf68e48f05b41bb7621990c3b (patch) | |
| tree | 9cbd2d7624ce02938397eec92404c4a5d6147893 /Source | |
| parent | 51d9bd30cdf3ec7212b06c56acb5cdd1fc1e325c (diff) | |
Don't set logic to UFNIA when /useArrayTheory
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 7 |
1 files changed, 7 insertions, 0 deletions
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);
}
|