Name type to regain macOS 10.14.6 compatibility

tautschnig · tautschnig · commit 31745494221e · 2023-03-07T12:58:09.000Z
Avoid (spurious) ambiguity by explicitly naming the type to be constructed. This seems to be required by the compiler shipped with macOS 10.14.6. Fixes: #7464
diff --git a/src/solvers/smt2_incremental/smt_response_validation.cpp b/src/solvers/smt2_incremental/smt_response_validation.cpp
@@ -310,7 +310,10 @@ validate_valuation_pair(
       smt_to_smt2_string(valid_descriptor.get_sort()) + "\nValue has sort " +
       smt_to_smt2_string(valid_value.get_sort())};
   }
-  return resultt{{valid_descriptor, valid_value}};
+  // see https://github.com/diffblue/cbmc/issues/7464 for why we explicitly name
+  // the valuation_pairt type here:
+  return resultt{
+    smt_get_value_responset::valuation_pairt{valid_descriptor, valid_value}};
 }
 
 /// \returns: A response or error in the case where the parse tree appears to be

Original file line number	Diff line number	Diff line change
`@@ -310,7 +310,10 @@ validate_valuation_pair(`
`310`	`310`	`smt_to_smt2_string(valid_descriptor.get_sort()) + "\nValue has sort " +`
`311`	`311`	`smt_to_smt2_string(valid_value.get_sort())};`
`312`	`312`	`}`
`313`		`- return resultt{{valid_descriptor, valid_value}};`
	`313`	`+ // see https://github.com/diffblue/cbmc/issues/7464 for why we explicitly name`
	`314`	`+ // the valuation_pairt type here:`
	`315`	`+ return resultt{`
	`316`	`+ smt_get_value_responset::valuation_pairt{valid_descriptor, valid_value}};`
`314`	`317`	`}`
`315`	`318`
`316`	`319`	`/// \returns: A response or error in the case where the parse tree appears to be`