Fix get-model when sort constructors are present (#7828)

Fixes a spurious error on kind benchmarks.

Note that we don't properly handle instantiated sort constructors currently, which I believe need to be handled as declared sorts when calling getModel.

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 7cd475cbb745cb5f8edab6e7b67836e0135e54b1..1321c558e5b1d20653b2ff722e5cefa456e17c6f 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1231,8 +1231,12 @@ size_t DeclareSortCommand::getArity() const { return d_arity; }
 api::Sort DeclareSortCommand::getSort() const { return d_sort; }
 void DeclareSortCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
-  // mark that it will be printed in the model
-  sm->addModelDeclarationSort(d_sort);
+  // mark that it will be printed in the model, if it is an uninterpreted
+  // sort (arity 0)
+  if (d_arity == 0)
+  {
+    sm->addModelDeclarationSort(d_sort);
+  }
   d_commandStatus = CommandSuccess::instance();
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4addbd8d1d218c5e864160564733cd43d542bf1a..4d8a7a65ff4778dc65b856eff763667747c51207 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -806,6 +806,7 @@ set(regress_0_tests
   regress0/parser/define_sort.smt2
   regress0/parser/force_logic_set_logic.smt2
   regress0/parser/force_logic_success.smt2
+  regress0/parser/get-model-sort-constructor.smt2
   regress0/parser/issue5163.smt2
   regress0/parser/issue6908-get-value-uc.smt2
   regress0/parser/issue7274.smt2

diff --git a/test/regress/regress0/parser/get-model-sort-constructor.smt2 b/test/regress/regress0/parser/get-model-sort-constructor.smt2
new file mode 100644 (file)
index 0000000..4f40e34
--- /dev/null
+++ b/test/regress/regress0/parser/get-model-sort-constructor.smt2
@@ -0,0 +1,8 @@
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: )
+(set-option :produce-models true)
+(set-logic QF_UFLIRA)
+(declare-sort FArray 2)
+(check-sat)
+(get-model)