Do not traverse quantifiers in nl ext purify (#3982)

1 files changed, 37 insertions, 0 deletions

diff --git a/test/regress/regress1/issue3970-nl-ext-purify.smt2 b/test/regress/regress1/issue3970-nl-ext-purify.smt2
new file mode 100644
index 000000000..5fbddf13d
--- /dev/null
+++ b/test/regress/regress1/issue3970-nl-ext-purify.smt2
@@ -0,0 +1,37 @@
+(set-logic QF_UFNRA)
+(set-option :nl-ext-purify true)
+(set-option :sygus-inference true)
+(set-info :status unsat)
+(declare-const v0 Bool)
+(declare-const v1 Bool)
+(declare-const v2 Bool)
+(declare-const v3 Bool)
+(declare-const v4 Bool)
+(declare-const v5 Bool)
+(declare-const v6 Bool)
+(declare-const v7 Bool)
+(declare-const v8 Bool)
+(declare-const v9 Bool)
+(declare-const r3 Real)
+(declare-const r5 Real)
+(assert v8)
+(declare-const v10 Bool)
+(assert (= 169 r5))
+(declare-const v11 Bool)
+(assert v5)
+(declare-const v12 Bool)
+(declare-const r7 Real)
+(assert (not v1))
+(assert v10)
+(declare-const v13 Bool)
+(declare-const r8 Real)
+(assert (not (distinct r7 (- (/ 0.816577 (+ r5 569703))) 0.0 r3)))
+(assert v4)
+(assert (and (distinct v3 v4 (= 169 r5) (= (+ r5 569703) (/ 0.816577 (+ r5 569703)) 0.816577 0.26205) v11 v7 (= 169 r5)) (> 0.816577 169 569703 0.26205) (distinct r7 (- (/ 0.816577 (+ r5 569703))) 0.0 r3) v3 (= (+ r5 569703) (/ 0.816577 (+ r5 569703)) 0.816577 0.26205) v5 v10))
+(declare-const v14 Bool)
+(assert (or (= (+ r5 569703) (/ 0.816577 (+ r5 569703)) 0.816577 0.26205) v6 (or (<= 0.26205 r7 353 569703) v7 v8 v13 v3) v5 v6 (distinct r7 (- (/ 0.816577 (+ r5 569703))) 0.0 r3)))
+(declare-const v15 Bool)
+(assert (xor v3 v11 v9 v3))
+(declare-const v16 Bool)
+(assert (xor v2 v8))
+(check-sat)