diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 3f5a0fcf1..1f4a86903 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -919,7 +919,6 @@ extern "C" {
case PR_REWRITE: return Z3_OP_PR_REWRITE;
case PR_REWRITE_STAR: return Z3_OP_PR_REWRITE_STAR;
case PR_PULL_QUANT: return Z3_OP_PR_PULL_QUANT;
- case PR_PULL_QUANT_STAR: return Z3_OP_PR_PULL_QUANT_STAR;
case PR_PUSH_QUANT: return Z3_OP_PR_PUSH_QUANT;
case PR_ELIM_UNUSED_VARS: return Z3_OP_PR_ELIM_UNUSED_VARS;
case PR_DER: return Z3_OP_PR_DER;
@@ -936,9 +935,7 @@ extern "C" {
case PR_IFF_OEQ: return Z3_OP_PR_IFF_OEQ;
case PR_NNF_POS: return Z3_OP_PR_NNF_POS;
case PR_NNF_NEG: return Z3_OP_PR_NNF_NEG;
- case PR_NNF_STAR: return Z3_OP_PR_NNF_STAR;
case PR_SKOLEMIZE: return Z3_OP_PR_SKOLEMIZE;
- case PR_CNF_STAR: return Z3_OP_PR_CNF_STAR;
case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ;
case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA;
case PR_HYPER_RESOLVE: return Z3_OP_PR_HYPER_RESOLVE;
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index 0726f9d53..9310d1e7d 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -932,7 +932,7 @@ namespace Microsoft.Z3
/// Indicates whether the term is a proof by condensed transitivity of a relation
///
///
- /// Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
+ /// Condensed transitivity proof.
/// It combines several symmetry and transitivity proofs.
/// Example:
/// T1: (R a b)
@@ -1035,14 +1035,11 @@ namespace Microsoft.Z3
///
///
/// A proof for rewriting an expression t into an expression s.
- /// This proof object is used if the parameter PROOF_MODE is 1.
/// This proof object can have n antecedents.
/// The antecedents are proofs for equalities used as substitution rules.
- /// The object is also used in a few cases if the parameter PROOF_MODE is 2.
- /// The cases are:
+ /// The object is used in a few cases:
/// - When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
/// - When converting bit-vectors to Booleans (BIT2BOOL=true)
- /// - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
///
public bool IsProofRewriteStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
@@ -1054,15 +1051,6 @@ namespace Microsoft.Z3
///
public bool IsProofPullQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }
- ///
- /// Indicates whether the term is a proof for pulling quantifiers out.
- ///
- ///
- /// A proof for (iff P Q) where Q is in prenex normal form.
- /// This proof object is only used if the parameter PROOF_MODE is 1.
- /// This proof object has no antecedents
- ///
- public bool IsProofPullQuantStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } }
///
/// Indicates whether the term is a proof for pushing quantifiers in.
@@ -1304,28 +1292,6 @@ namespace Microsoft.Z3
///
public bool IsProofNNFNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }
- ///
- /// Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
- ///
- ///
- /// A proof for (~ P Q) where Q is in negation normal form.
- ///
- /// This proof object is only used if the parameter PROOF_MODE is 1.
- ///
- /// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
- ///
- public bool IsProofNNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } }
-
- ///
- /// Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
- ///
- ///
- /// A proof for (~ P Q) where Q is in conjunctive normal form.
- /// This proof object is only used if the parameter PROOF_MODE is 1.
- /// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
- ///
- public bool IsProofCNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } }
-
///
/// Indicates whether the term is a proof for a Skolemization step
///
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 7b20b7993..db5c33e79 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -1398,8 +1398,7 @@ public class Expr extends AST
/**
* Indicates whether the term is a proof by condensed transitivity of a
* relation
- * Remarks: Condensed transitivity proof. This proof object is
- * only used if the parameter PROOF_MODE is 1. It combines several symmetry
+ * Remarks: Condensed transitivity proof. It combines several symmetry
* and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d)
* [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation.
*
@@ -1506,14 +1505,11 @@ public class Expr extends AST
/**
* Indicates whether the term is a proof by rewriting
* Remarks: A proof for
- * rewriting an expression t into an expression s. This proof object is used
- * if the parameter PROOF_MODE is 1. This proof object can have n
+ * rewriting an expression t into an expression s. This proof object can have n
* antecedents. The antecedents are proofs for equalities used as
- * substitution rules. The object is also used in a few cases if the
- * parameter PROOF_MODE is 2. The cases are: - When applying contextual
+ * substitution rules. The object is used in a few cases . The cases are: - When applying contextual
* simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to
- * Booleans (BIT2BOOL=true) - When pulling ite expression up
- * (PULL_CHEAP_ITE_TREES=true)
+ * Booleans (BIT2BOOL=true)
* @throws Z3Exception on error
* @return a boolean
**/
@@ -1534,17 +1530,6 @@ public class Expr extends AST
return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
}
- /**
- * Indicates whether the term is a proof for pulling quantifiers out.
- *
- * Remarks: A proof for (iff P Q) where Q is in prenex normal form. This * proof object is only used if the parameter PROOF_MODE is 1. This proof * object has no antecedents
- * @throws Z3Exception on error
- * @return a boolean
- **/
- public boolean isProofPullQuantStar()
- {
- return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR;
- }
/**
* Indicates whether the term is a proof for pushing quantifiers in.
@@ -1804,38 +1789,6 @@ public class Expr extends AST
return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG;
}
- /**
- * Indicates whether the term is a proof for (~ P Q) here Q is in negation
- * normal form.
- * Remarks: A proof for (~ P Q) where Q is in negation normal
- * form.
- *
- * This proof object is only used if the parameter PROOF_MODE is 1.
- *
- * This proof object may have n antecedents. Each antecedent is a
- * PR_DEF_INTRO.
- * @throws Z3Exception on error
- * @return a boolean
- **/
- public boolean isProofNNFStar()
- {
- return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_STAR;
- }
-
- /**
- * Indicates whether the term is a proof for (~ P Q) where Q is in
- * conjunctive normal form.
- * Remarks: A proof for (~ P Q) where Q is in
- * conjunctive normal form. This proof object is only used if the parameter
- * PROOF_MODE is 1. This proof object may have n antecedents. Each
- * antecedent is a PR_DEF_INTRO.
- * @throws Z3Exception on error
- * @return a boolean
- **/
- public boolean isProofCNFStar()
- {
- return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR;
- }
/**
* Indicates whether the term is a proof for a Skolemization step
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index f7c218963..88d6aa1cf 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -459,7 +459,7 @@ typedef enum
[trans T1 T2]: (R t u)
}
- - Z3_OP_PR_TRANSITIVITY_STAR: Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
+ - Z3_OP_PR_TRANSITIVITY_STAR: Condensed transitivity proof.
It combines several symmetry and transitivity proofs.
Example:
@@ -539,21 +539,14 @@ typedef enum
}
- Z3_OP_PR_REWRITE_STAR: A proof for rewriting an expression t into an expression s.
- This proof object is used if the parameter PROOF_MODE is 1.
This proof object can have n antecedents.
The antecedents are proofs for equalities used as substitution rules.
- The object is also used in a few cases if the parameter PROOF_MODE is 2.
- The cases are:
+ The proof rule is used in a few cases. The cases are:
- When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
- When converting bit-vectors to Booleans (BIT2BOOL=true)
- - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
- Z3_OP_PR_PULL_QUANT: A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
- - Z3_OP_PR_PULL_QUANT_STAR: A proof for (iff P Q) where Q is in prenex normal form.
- This proof object is only used if the parameter PROOF_MODE is 1.
- This proof object has no antecedents.
-
- Z3_OP_PR_PUSH_QUANT: A proof for:
\nicebox{
@@ -726,15 +719,6 @@ typedef enum
[nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
(and (or r_1 r_2) (or r_1' r_2')))
}
- - Z3_OP_PR_NNF_STAR: A proof for (~ P Q) where Q is in negation normal form.
-
- This proof object is only used if the parameter PROOF_MODE is 1.
-
- This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
-
- - Z3_OP_PR_CNF_STAR: A proof for (~ P Q) where Q is in conjunctive normal form.
- This proof object is only used if the parameter PROOF_MODE is 1.
- This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
- Z3_OP_PR_SKOLEMIZE: Proof for:
@@ -1142,7 +1126,6 @@ typedef enum {
Z3_OP_PR_REWRITE,
Z3_OP_PR_REWRITE_STAR,
Z3_OP_PR_PULL_QUANT,
- Z3_OP_PR_PULL_QUANT_STAR,
Z3_OP_PR_PUSH_QUANT,
Z3_OP_PR_ELIM_UNUSED_VARS,
Z3_OP_PR_DER,
@@ -1159,8 +1142,6 @@ typedef enum {
Z3_OP_PR_IFF_OEQ,
Z3_OP_PR_NNF_POS,
Z3_OP_PR_NNF_NEG,
- Z3_OP_PR_NNF_STAR,
- Z3_OP_PR_CNF_STAR,
Z3_OP_PR_SKOLEMIZE,
Z3_OP_PR_MODUS_PONENS_OEQ,
Z3_OP_PR_TH_LEMMA,
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 127967374..7e143e1a3 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -663,7 +663,6 @@ basic_decl_plugin::basic_decl_plugin():
m_not_or_elim_decl(nullptr),
m_rewrite_decl(nullptr),
m_pull_quant_decl(nullptr),
- m_pull_quant_star_decl(nullptr),
m_push_quant_decl(nullptr),
m_elim_unused_vars_decl(nullptr),
m_der_decl(nullptr),
@@ -827,7 +826,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
case PR_REWRITE: return mk_proof_decl("rewrite", k, 0, m_rewrite_decl);
case PR_REWRITE_STAR: return mk_proof_decl("rewrite*", k, num_parents, m_rewrite_star_decls);
case PR_PULL_QUANT: return mk_proof_decl("pull-quant", k, 0, m_pull_quant_decl);
- case PR_PULL_QUANT_STAR: return mk_proof_decl("pull-quant*", k, 0, m_pull_quant_star_decl);
case PR_PUSH_QUANT: return mk_proof_decl("push-quant", k, 0, m_push_quant_decl);
case PR_ELIM_UNUSED_VARS: return mk_proof_decl("elim-unused", k, 0, m_elim_unused_vars_decl);
case PR_DER: return mk_proof_decl("der", k, 0, m_der_decl);
@@ -844,8 +842,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
case PR_IFF_OEQ: return mk_proof_decl("iff~", k, 1, m_iff_oeq_decl);
case PR_NNF_POS: return mk_proof_decl("nnf-pos", k, num_parents, m_nnf_pos_decls);
case PR_NNF_NEG: return mk_proof_decl("nnf-neg", k, num_parents, m_nnf_neg_decls);
- case PR_NNF_STAR: return mk_proof_decl("nnf*", k, num_parents, m_nnf_star_decls);
- case PR_CNF_STAR: return mk_proof_decl("cnf*", k, num_parents, m_cnf_star_decls);
case PR_SKOLEMIZE: return mk_proof_decl("sk", k, 0, m_skolemize_decl);
case PR_MODUS_PONENS_OEQ: return mk_proof_decl("mp~", k, 2, m_mp_oeq_decl);
case PR_TH_LEMMA: return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_decls);
@@ -949,7 +945,6 @@ void basic_decl_plugin::finalize() {
DEC_REF(m_not_or_elim_decl);
DEC_REF(m_rewrite_decl);
DEC_REF(m_pull_quant_decl);
- DEC_REF(m_pull_quant_star_decl);
DEC_REF(m_push_quant_decl);
DEC_REF(m_elim_unused_vars_decl);
DEC_REF(m_der_decl);
@@ -975,8 +970,6 @@ void basic_decl_plugin::finalize() {
DEC_ARRAY_REF(m_apply_def_decls);
DEC_ARRAY_REF(m_nnf_pos_decls);
DEC_ARRAY_REF(m_nnf_neg_decls);
- DEC_ARRAY_REF(m_nnf_star_decls);
- DEC_ARRAY_REF(m_cnf_star_decls);
DEC_ARRAY_REF(m_th_lemma_decls);
DEC_REF(m_hyper_res_decl0);
@@ -2844,12 +2837,6 @@ proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) {
return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q));
}
-proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) {
- if (proofs_disabled())
- return nullptr;
- return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q));
-}
-
proof * ast_manager::mk_push_quant(quantifier * q, expr * e) {
if (proofs_disabled())
return nullptr;
@@ -3094,15 +3081,6 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof *
return mk_app(m_basic_family_id, PR_NNF_NEG, args.size(), args.c_ptr());
}
-proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
- if (proofs_disabled())
- return nullptr;
- ptr_buffer args;
- args.append(num_proofs, (expr**) proofs);
- args.push_back(mk_oeq(s, t));
- return mk_app(m_basic_family_id, PR_NNF_STAR, args.size(), args.c_ptr());
-}
-
proof * ast_manager::mk_skolemization(expr * q, expr * e) {
if (proofs_disabled())
return nullptr;
@@ -3111,15 +3089,6 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) {
return mk_app(m_basic_family_id, PR_SKOLEMIZE, mk_oeq(q, e));
}
-proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
- if (proofs_disabled())
- return nullptr;
- ptr_buffer args;
- args.append(num_proofs, (expr**) proofs);
- args.push_back(mk_oeq(s, t));
- return mk_app(m_basic_family_id, PR_CNF_STAR, args.size(), args.c_ptr());
-}
-
proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
if (proofs_disabled())
return nullptr;
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 55fea1b69..68e02d791 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1042,11 +1042,11 @@ enum basic_op_kind {
PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO,
PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT,
- PR_PULL_QUANT_STAR, PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST,
+ PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST,
PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_AXIOM,
- PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_NNF_STAR, PR_SKOLEMIZE, PR_CNF_STAR,
+ PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_SKOLEMIZE,
PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, PR_HYPER_RESOLVE, LAST_BASIC_PR
};
@@ -1080,7 +1080,6 @@ protected:
func_decl * m_not_or_elim_decl;
func_decl * m_rewrite_decl;
func_decl * m_pull_quant_decl;
- func_decl * m_pull_quant_star_decl;
func_decl * m_push_quant_decl;
func_decl * m_elim_unused_vars_decl;
func_decl * m_der_decl;
@@ -1106,8 +1105,6 @@ protected:
ptr_vector m_apply_def_decls;
ptr_vector m_nnf_pos_decls;
ptr_vector m_nnf_neg_decls;
- ptr_vector m_nnf_star_decls;
- ptr_vector m_cnf_star_decls;
ptr_vector m_th_lemma_decls;
func_decl * m_hyper_res_decl0;
@@ -2182,7 +2179,6 @@ public:
proof * mk_oeq_rewrite(expr * s, expr * t);
proof * mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
proof * mk_pull_quant(expr * e, quantifier * q);
- proof * mk_pull_quant_star(expr * e, quantifier * q);
proof * mk_push_quant(quantifier * q, expr * e);
proof * mk_elim_unused_vars(quantifier * q, expr * r);
proof * mk_der(quantifier * q, expr * r);
@@ -2201,9 +2197,8 @@ public:
proof * mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
proof * mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
- proof * mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
proof * mk_skolemization(expr * q, expr * e);
- proof * mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
+
proof * mk_and_elim(proof * p, unsigned i);
proof * mk_not_or_elim(proof * p, unsigned i);
diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp
index bd50e6c2a..0e16abd11 100644
--- a/src/ast/proofs/proof_checker.cpp
+++ b/src/ast/proofs/proof_checker.cpp
@@ -440,16 +440,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m););
return false;
}
- case PR_PULL_QUANT_STAR: {
- if (match_proof(p) &&
- match_fact(p, fact) &&
- match_iff(fact.get(), t1, t2)) {
- // TBD: check the enchilada.
- return true;
- }
- IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence:\n" << mk_bounded_pp(p, m););
- return false;
- }
case PR_PUSH_QUANT: {
if (match_proof(p) &&
match_fact(p, fact) &&
@@ -730,10 +720,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
// TBD:
return true;
}
- case PR_NNF_STAR: {
- // TBD:
- return true;
- }
case PR_SKOLEMIZE: {
// (exists ?x (p ?x y)) -> (p (sk y) y)
// (not (forall ?x (p ?x y))) -> (not (p (sk y) y))
@@ -755,19 +741,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
UNREACHABLE();
return false;
}
- case PR_CNF_STAR: {
- for (unsigned i = 0; i < proofs.size(); ++i) {
- if (match_op(proofs[i].get(), PR_DEF_INTRO, terms)) {
- // ok
- }
- else {
- UNREACHABLE();
- return false;
- }
- }
- // coarse grain CNF conversion.
- return true;
- }
case PR_MODUS_PONENS_OEQ: {
if (match_fact(p, fact) &&
match_proof(p, p0, p1) &&
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 3393634b6..46388fcf4 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -597,7 +597,6 @@ namespace smt {
void theory_arith::mk_to_int_axiom(app * n) {
SASSERT(m_util.is_to_int(n));
ast_manager & m = get_manager();
- context & ctx = get_context();
expr* x = n->get_arg(0);
// to_int (to_real x) = x
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 9dfd0475b..3335370eb 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -5595,6 +5595,8 @@ namespace smt {
// merge arg0 and arg1
expr * arg0 = to_app(node)->get_arg(0);
expr * arg1 = to_app(node)->get_arg(1);
+ SASSERT(arg0 != node);
+ SASSERT(arg1 != node);
expr * arg0DeAlias = dealias_node(arg0, varAliasMap, concatAliasMap);
expr * arg1DeAlias = dealias_node(arg1, varAliasMap, concatAliasMap);
get_grounded_concats(arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 6ad9c0812..93a0b2e88 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -582,7 +582,7 @@ struct ctx_simplify_tactic::imp {
for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
expr * t = g.form(i);
process(t, r);
- proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(t, r, 0, nullptr)); // TODO :-)
+ proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(t, r));
g.update(i, r, new_pr, g.dep(i));
}
}
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index e8d3150af..47f96a7d9 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -382,7 +382,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
change |= r != g.form(i);
proof* new_pr = nullptr;
if (g.proofs_enabled()) {
- new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, nullptr));
+ new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r));
}
g.update(i, r, new_pr, g.dep(i));
}
@@ -402,7 +402,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
proof* new_pr = nullptr;
if (g.proofs_enabled()) {
- new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, nullptr));
+ new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r));
}
g.update(i, r, new_pr, g.dep(i));
}