Do not eliminate extended arithmetic symbols when finite model finding is on, add...

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index a5ecc8e7256a4d25e0ccd36d40f360d80965c96f..f15723e085730dbaaa054ce7dc44ac9599b7d084 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -54,7 +54,7 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
  perform aggressive miniscoping for quantifiers
 option elimTautQuant --elim-taut-quant bool :default true
  eliminate tautological disjuncts of quantified formulas
-option elimExtArithQuant --elim-ext-arith-quant bool :default true
+option elimExtArithQuant --elim-ext-arith-quant bool :read-write :default true
  eliminate extended arithmetic symbols in quantified formulas
 option condRewriteQuant --cond-rewrite-quant bool :default true
  conditional rewriting of quantified formulas

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 16da6691cee931158bd23cb312eccf29d855393e..4e75a79371cbaf4b08b93aa571d9818d4aad51c7 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1781,11 +1781,15 @@ void SmtEngine::setDefaults() {
     if( !options::quantDynamicSplit.wasSetByUser() ){
       options::quantDynamicSplit.set( quantifiers::QUANT_DSPLIT_MODE_DEFAULT );
     }
+    //do not eliminate extended arithmetic symbols from quantified formulas
+    if( !options::elimExtArithQuant.wasSetByUser() ){
+      options::elimExtArithQuant.set( false );
+    }
     if( !options::eMatching.wasSetByUser() ){
       options::eMatching.set( options::fmfInstEngine() );
     }
     if( !options::instWhenMode.wasSetByUser() ){
-      //instantiate only on last call  FIXME: remove?
+      //instantiate only on last call
       if( options::eMatching() ){
         options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
       }

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 593cdfa8b03b893e01d58b9255ad496dc868b6c2..b02443989b7aa48a14f9af46dad3dbd6cfff8cb2 100644 (file)
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -73,7 +73,8 @@ TESTS =       \
        constr-ground-to.smt2 \
        bug-041417-set-options.cvc \
        alg202+1.smt2 \
-       fmf-fun-no-elim-ext-arith.smt2
+       fmf-fun-no-elim-ext-arith.smt2 \
+       fmf-fun-no-elim-ext-arith2.smt2
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2 b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2
new file mode 100644 (file)
index 0000000..ea5a5e4
--- /dev/null
+++ b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2
@@ -0,0 +1,25 @@
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+(set-logic UFLIA)
+(set-info :status sat)
+(define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool (
+    or
+    (= n1 n 0)
+    (= n2 n 0)
+    (
+        and
+        (> n1 0)
+        (> n2 0)
+        (>= n 0)
+        (= (not (= (mod n 2 ) 0)) (and (not (= (mod n1 2 ) 0)) (not (= (mod n2 2) 0))))
+        (int-and (div n 2) (div n1 2) (div n2 2))
+    )
+))
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(assert (= x 1))
+(assert (= y 1))
+(assert (= z 1))
+(assert (int-and z x y))
+(check-sat)