bug fix when using multiple sorts for IntegerFourierMotzkin

vprover · Jan 31, 2025 · d73b091 · d73b091
1 parent bd08729
commit d73b091
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/Inferences/ALASCA/IntegerFourierMotzkin.hpp b/Inferences/ALASCA/IntegerFourierMotzkin.hpp
@@ -59,6 +59,7 @@ struct IntegerFourierMotzkinConf
       Premise2 const& prem2, unsigned varBank2,
       AbstractingUnifier& uwa) const
   {
+    if (!prem0.numTraitsIs<NumTraits>()) return {};
     auto sigma2 = [&](auto t)  { return uwa.subs().apply(t, varBank2); };
     return applyRule__(prem0, varBank0,
                        prem1, varBank1,

diff --git a/Kernel/ALASCA/SelectionPrimitves.hpp b/Kernel/ALASCA/SelectionPrimitves.hpp
@@ -106,6 +106,10 @@ namespace Kernel {
           .apply([this](auto& lit) 
               { return AnyConstantType(lit.term().summandAt(_term).numeral); }); }
 
+    template<class NumTraits>
+    bool numTraitsIs() const 
+    { return numeral().is<typename NumTraits::ConstantType>(); }
+
     template<class NumTraits>
     auto numeral() const 
     { return numeral().unwrap<typename NumTraits::ConstantType>(); }