Fix issue with multiple infinities in CEGQI for LIRA (#4114)

Fixes #4086.

Quantifier instantiation involves two symbolic representations of infinities for real and int and was not handled correctly previously.

diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
index 11c126eafea4a6555cc8ca606c8133f73feecaa9..91f65c4ef71eaa7f5c2431a2a8ec7992421a4b97 100644 (file)
--- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -144,7 +144,7 @@ Node VtsTermCache::rewriteVtsSymbols(Node n)
           std::vector<Node> subs_lhs;
           subs_lhs.push_back(inf);
           std::vector<Node> subs_rhs;
-          subs_lhs.push_back(rew_vts_inf);
+          subs_rhs.push_back(rew_vts_inf);
           n = n.substitute(subs_lhs.begin(),
                            subs_lhs.end(),
                            subs_rhs.begin(),

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d822ce1572f1b24e5e9712d0f77df912b55f8656..bffb2c4db6d8308413338c0421d92c776ff91c98 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -724,6 +724,7 @@ set(regress_0_tests
   regress0/quantifiers/issue2033-macro-arith.smt2
   regress0/quantifiers/issue2035.smt2
   regress0/quantifiers/issue3655.smt2
+  regress0/quantifiers/issue4086-infs.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macros-int-real.smt2
   regress0/quantifiers/macros-real-arg.smt2

diff --git a/test/regress/regress0/quantifiers/issue4086-infs.smt2 b/test/regress/regress0/quantifiers/issue4086-infs.smt2
new file mode 100644 (file)
index 0000000..2ebb459
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue4086-infs.smt2
@@ -0,0 +1,7 @@
+(set-logic LIRA)
+(set-info :status unsat)
+(set-option :cbqi-use-inf-int true) 
+(set-option :cbqi-use-inf-real true)
+(set-option :var-ineq-elim-quant false) 
+(assert (forall (( b Real )) (forall (( c Int )) (and  (> c (* b 2 ))))))
+(check-sat)