summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers/SMTLib')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs7
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);
}