From b7dcbee6f351c22ca3454d706d5773d01dd806fa Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 15 Apr 2021 14:57:53 -0700
Subject: preprocessing context: Add wrapper for model substitutions. (#6370)

Previously, preprocessing passes added model substitutions without
expanding definitions for substitutions, which can be a problem.
This adds a wrapper function to take care of it properly.

Fixes #5473.
---
 test/regress/regress0/issue5473.smt2 | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test/regress/regress0/issue5473.smt2

(limited to 'test/regress/regress0/issue5473.smt2')

diff --git a/test/regress/regress0/issue5473.smt2 b/test/regress/regress0/issue5473.smt2
new file mode 100644
index 000000000..bf24726f9
--- /dev/null
+++ b/test/regress/regress0/issue5473.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+; EXPECT: ((baz true))
+(set-logic QF_NIRA)
+(set-option :produce-models true)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(assert (! (or (= a (div 0 b))) :named baz))
+(assert (and (< b 5)))
+(check-sat)
+(get-assignment)
-- 
cgit v1.2.3