From e3e6f0dc62f0bb9d3fb8d752c5eb4600872fd806 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 4 Jan 2020 13:24:14 -0600
Subject: [PATCH] Fix finiteness check for bounded fmf (#3589)

Recently, finite model finding via uninterpreted sorts was decoupled from finite bound inference techniques (the BoundedIntegers module in theory/quantifiers/fmf/). This module assumed that finite model finding was enabled in one place. This fixes the issue by adding an additional check. This fixes a model unsoundness issue where bounds on an uninterpreted sort were not being enforced.

This fixes #3587.
---
 src/theory/quantifiers/fmf/bounded_integers.cpp  | 2 +-
 test/regress/CMakeLists.txt                      | 1 +
 test/regress/regress1/fmf/issue3587.smt2         | 9 +++++++++
 test/regress/regress1/quantifiers/issue3537.smt2 | 2 +-
 4 files changed, 12 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress1/fmf/issue3587.smt2

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index cfff64f15..2bcb154a0 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -409,7 +409,7 @@ void BoundedIntegers::checkOwnership(Node f)
       for( unsigned i=0; i<f[0].getNumChildren(); i++) {
         if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
           TypeNode tn = f[0][i].getType();
-          if (tn.isSort()
+          if ((tn.isSort() && tn.isInterpretedFinite())
               || d_quantEngine->getTermEnumeration()->mayComplete(tn))
           {
             success = true;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e27cff94d..b42d586c8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1222,6 +1222,7 @@ set(regress_1_tests
   regress1/fmf/german169.smt2
   regress1/fmf/german73.smt2
   regress1/fmf/issue2034-preinit.smt2
+  regress1/fmf/issue3587.smt2
   regress1/fmf/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2
   regress1/fmf/ko-bound-set.cvc
diff --git a/test/regress/regress1/fmf/issue3587.smt2 b/test/regress/regress1/fmf/issue3587.smt2
new file mode 100644
index 000000000..5ca5e4f16
--- /dev/null
+++ b/test/regress/regress1/fmf/issue3587.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: unknown
+(set-logic ALL)
+(declare-sort a 0) 
+(declare-datatypes ((prod 0)) (((Pair (gx a) (gy a))))) 
+(declare-fun p () prod) 
+(assert (forall ((x a) (y a)) (not (= p (Pair x y))))) 
+; problem is unsat, currently unknown with fmf-bound
+(check-sat)  
diff --git a/test/regress/regress1/quantifiers/issue3537.smt2 b/test/regress/regress1/quantifiers/issue3537.smt2
index 08f929c4c..2024153ad 100644
--- a/test/regress/regress1/quantifiers/issue3537.smt2
+++ b/test/regress/regress1/quantifiers/issue3537.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --no-check-models
+; COMMAND-LINE: --strings-exp --no-check-models --finite-model-find
 ; EXPECT: sat
 (set-logic ALL)
 (declare-datatypes ((UNIT 0)) (((Unit))
-- 
2.30.2