diff -r aeb797356de0 -r b6239ed66b94 src/HOL/Tools/SMT/verit_proof.ML
--- a/src/HOL/Tools/SMT/verit_proof.ML	Mon Jun 13 20:02:00 2022 +0200
+++ b/src/HOL/Tools/SMT/verit_proof.ML	Tue Jun 14 16:14:28 2022 +0200
@@ -55,6 +55,7 @@
   val theory_resolution2_rule: string
   val equiv_pos2_rule: string
   val th_resolution_rule: string
+  val and_pos_rule: string
 
   val is_skolemization: string -> bool
   val is_skolemization_step: veriT_replay_node -> bool
@@ -248,11 +249,12 @@
 val theory_resolution2_rule = "__theory_resolution2" (*arbitrary*)
 val equiv_pos2_rule = "equiv_pos2"
 val th_resolution_rule = "th_resolution"
+val and_pos_rule = "and_pos"
 
 val skolemization_steps = ["sko_forall", "sko_ex"]
 val is_skolemization = member (op =) skolemization_steps
-val keep_app_symbols = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule]
-val keep_raw_lifting = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule]
+val keep_app_symbols = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule, and_pos_rule]
+val keep_raw_lifting = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule, and_pos_rule]
 val is_SH_trivial = member (op =) [not_not_rule, contract_rule]
 
 fun is_skolemization_step (VeriT_Replay_Node {id, ...}) = is_skolemization id