Merge pull request #7580 from tautschnig/cleanup/7464-type-lookup

tautschnig · web-flow · commit f6898d4e7c36 · 2023-03-07T16:03:15.000+01:00
Name type to regain macOS 10.14.6 compatibility
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`