Propositions used in expressions are defined twice in discharge

[UnsignedByte]

Propositions that are used in expressions (namely in the ternary operation) are defined twice. This does not cause problems with z3 (I assume it is overridden by the second definition, but as both are equal nothing bad happens), but cvc5 has issues when this occurs.

filament/crates/filament/src/ir_passes/discharge.rs

Lines 619 to 631 in e0703dd

	let relevant_props = idx
	.relevant_props(&data.comp)
	.into_iter()
	.map(|i| (i, data.comp.get(i)));
	for (pidx, prop) in relevant_props {
	let assign = self.prop_to_sexp(prop);
	let sexp = self
	.sol
	.define_const(Discharge::fmt_prop(pidx), bs, assign)
	.unwrap();
	self.prop_map.insert(pidx, SExprWrapper::SExpr(sexp));
	}

Every proposition is added again here:

filament/crates/filament/src/ir_passes/discharge.rs

Lines 673 to 688 in e0703dd

	for (idx, prop) in data
	.comp
	.props()
	.iter()
	.filter(|(idx, _)| idx.valid(&data.comp))
	{
	// Define assertion equating the proposition to its assignment
	let assign = self.prop_to_sexp(prop);
	if let Ok(sexp) =
	self.sol.define_const(Discharge::fmt_prop(idx), bs, assign)
	{
	self.prop_map.insert(idx, SExprWrapper::SExpr(sexp));
	}
	}
	// Pass does not need to traverse the control program.
	Action::Continue

In CVC5 we get

[TRACE] -> (define-fun prop12 () Bool (> e37 e57))
[TRACE] <- (error "Parse Error: <shell>:1.13: Symbol 'prop12' previously declared as a variable")