Refactor to deduplicate shared bit vector validation code

thomasspriggs · thomasspriggs · commit 53c53f329a07 · 2022-02-14T17:35:24.000Z
diff --git a/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp b/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp
@@ -19,14 +19,33 @@ smt_sortt smt_bit_vector_theoryt::concatt::return_sort(
   return smt_bit_vector_sortt{get_width(lhs) + get_width(rhs)};
 }
 
+static void validate_bit_vector_sort(
+  const std::string &descriptor,
+  const smt_termt &operand)
+{
+  const auto operand_sort = operand.get_sort().cast<smt_bit_vector_sortt>();
+  INVARIANT(
+    operand_sort,
+    descriptor + " operand is expected to have a bit-vector sort.");
+}
+
+static void validate_bit_vector_sort(const smt_termt &operand)
+{
+  validate_bit_vector_sort("The", operand);
+}
+
+static void
+validate_bit_vector_sorts(const smt_termt &lhs, const smt_termt &rhs)
+{
+  validate_bit_vector_sort("Left", lhs);
+  validate_bit_vector_sort("Right", rhs);
+}
+
 void smt_bit_vector_theoryt::concatt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  const auto lhs_sort = lhs.get_sort().cast<smt_bit_vector_sortt>();
-  INVARIANT(lhs_sort, "Left operand must have bitvector sort.");
-  const auto rhs_sort = rhs.get_sort().cast<smt_bit_vector_sortt>();
-  INVARIANT(rhs_sort, "Right operand must have bitvector sort.");
+  validate_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::concatt>
@@ -63,18 +82,14 @@ smt_bit_vector_theoryt::extract(std::size_t i, std::size_t j)
   return smt_function_application_termt::factoryt<extractt>(i, j);
 }
 
-static void validate_bit_vector_operator_arguments(
-  const smt_termt &left,
-  const smt_termt &right)
+static void
+validate_matched_bit_vector_sorts(const smt_termt &left, const smt_termt &right)
 {
-  const auto left_sort = left.get_sort().cast<smt_bit_vector_sortt>();
-  INVARIANT(left_sort, "Left operand must have bitvector sort.");
-  const auto right_sort = right.get_sort().cast<smt_bit_vector_sortt>();
-  INVARIANT(right_sort, "Right operand must have bitvector sort.");
+  validate_bit_vector_sorts(left, right);
   // The below invariant is based on the smtlib standard.
   // See http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV
   INVARIANT(
-    left_sort->bit_width() == right_sort->bit_width(),
+    left.get_sort() == right.get_sort(),
     "Left and right operands must have the same bit width.");
 }
 
@@ -92,8 +107,7 @@ smt_sortt smt_bit_vector_theoryt::nott::return_sort(const smt_termt &operand)
 
 void smt_bit_vector_theoryt::nott::validate(const smt_termt &operand)
 {
-  const auto operand_sort = operand.get_sort().cast<smt_bit_vector_sortt>();
-  INVARIANT(operand_sort, "The operand is expected to have a bit-vector sort.");
+  validate_bit_vector_sort(operand);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nott>
@@ -115,7 +129,7 @@ void smt_bit_vector_theoryt::andt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::andt>
@@ -137,7 +151,7 @@ void smt_bit_vector_theoryt::ort::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::ort>
@@ -159,7 +173,7 @@ void smt_bit_vector_theoryt::nandt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nandt>
@@ -181,7 +195,7 @@ void smt_bit_vector_theoryt::nort::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nort>
@@ -203,7 +217,7 @@ void smt_bit_vector_theoryt::xort::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::xort>
@@ -225,7 +239,7 @@ void smt_bit_vector_theoryt::xnort::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::xnort>
@@ -249,7 +263,7 @@ void smt_bit_vector_theoryt::unsigned_less_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -272,7 +286,7 @@ void smt_bit_vector_theoryt::unsigned_less_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -295,7 +309,7 @@ void smt_bit_vector_theoryt::unsigned_greater_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -319,7 +333,7 @@ void smt_bit_vector_theoryt::unsigned_greater_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -342,7 +356,7 @@ void smt_bit_vector_theoryt::signed_less_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -365,7 +379,7 @@ void smt_bit_vector_theoryt::signed_less_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -388,7 +402,7 @@ void smt_bit_vector_theoryt::signed_greater_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -411,7 +425,7 @@ void smt_bit_vector_theoryt::signed_greater_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -434,7 +448,7 @@ void smt_bit_vector_theoryt::addt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::addt>
@@ -456,7 +470,7 @@ void smt_bit_vector_theoryt::subtractt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -479,7 +493,7 @@ void smt_bit_vector_theoryt::multiplyt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -502,7 +516,7 @@ void smt_bit_vector_theoryt::unsigned_dividet::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -525,7 +539,7 @@ void smt_bit_vector_theoryt::signed_dividet::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -548,7 +562,7 @@ void smt_bit_vector_theoryt::unsigned_remaindert::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -571,7 +585,7 @@ void smt_bit_vector_theoryt::signed_remaindert::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -590,8 +604,7 @@ smt_sortt smt_bit_vector_theoryt::negatet::return_sort(const smt_termt &operand)
 
 void smt_bit_vector_theoryt::negatet::validate(const smt_termt &operand)
 {
-  const auto operand_sort = operand.get_sort().cast<smt_bit_vector_sortt>();
-  INVARIANT(operand_sort, "The operand is expected to have a bit-vector sort.");
+  validate_bit_vector_sort(operand);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::negatet>
@@ -613,7 +626,7 @@ void smt_bit_vector_theoryt::shift_leftt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -636,7 +649,7 @@ void smt_bit_vector_theoryt::logical_shift_rightt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -659,7 +672,7 @@ void smt_bit_vector_theoryt::arithmetic_shift_rightt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_operator_arguments(lhs, rhs);
+  validate_matched_bit_vector_sorts(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<

Original file line number	Diff line number	Diff line change
`@@ -19,14 +19,33 @@ smt_sortt smt_bit_vector_theoryt::concatt::return_sort(`
`19`	`19`	`return smt_bit_vector_sortt{get_width(lhs) + get_width(rhs)};`
`20`	`20`	`}`
`21`	`21`
	`22`	`+static void validate_bit_vector_sort(`
	`23`	`+ const std::string &descriptor,`
	`24`	`+ const smt_termt &operand)`
	`25`	`+{`
	`26`	`+ const auto operand_sort = operand.get_sort().cast<smt_bit_vector_sortt>();`
	`27`	`+ INVARIANT(`
	`28`	`+ operand_sort,`
	`29`	`+ descriptor + " operand is expected to have a bit-vector sort.");`
	`30`	`+}`
	`31`	`+`
	`32`	`+static void validate_bit_vector_sort(const smt_termt &operand)`
	`33`	`+{`
	`34`	`+ validate_bit_vector_sort("The", operand);`
	`35`	`+}`
	`36`	`+`
	`37`	`+static void`
	`38`	`+validate_bit_vector_sorts(const smt_termt &lhs, const smt_termt &rhs)`
	`39`	`+{`
	`40`	`+ validate_bit_vector_sort("Left", lhs);`
	`41`	`+ validate_bit_vector_sort("Right", rhs);`
	`42`	`+}`
	`43`	`+`
`22`	`44`	`void smt_bit_vector_theoryt::concatt::validate(`
`23`	`45`	`const smt_termt &lhs,`
`24`	`46`	`const smt_termt &rhs)`
`25`	`47`	`{`
`26`		`- const auto lhs_sort = lhs.get_sort().cast<smt_bit_vector_sortt>();`
`27`		`- INVARIANT(lhs_sort, "Left operand must have bitvector sort.");`
`28`		`- const auto rhs_sort = rhs.get_sort().cast<smt_bit_vector_sortt>();`
`29`		`- INVARIANT(rhs_sort, "Right operand must have bitvector sort.");`
	`48`	`+ validate_bit_vector_sorts(lhs, rhs);`
`30`	`49`	`}`
`31`	`50`
`32`	`51`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::concatt>`
`@@ -63,18 +82,14 @@ smt_bit_vector_theoryt::extract(std::size_t i, std::size_t j)`
`63`	`82`	`return smt_function_application_termt::factoryt<extractt>(i, j);`
`64`	`83`	`}`
`65`	`84`
`66`		`-static void validate_bit_vector_operator_arguments(`
`67`		`- const smt_termt &left,`
`68`		`- const smt_termt &right)`
	`85`	`+static void`
	`86`	`+validate_matched_bit_vector_sorts(const smt_termt &left, const smt_termt &right)`
`69`	`87`	`{`
`70`		`- const auto left_sort = left.get_sort().cast<smt_bit_vector_sortt>();`
`71`		`- INVARIANT(left_sort, "Left operand must have bitvector sort.");`
`72`		`- const auto right_sort = right.get_sort().cast<smt_bit_vector_sortt>();`
`73`		`- INVARIANT(right_sort, "Right operand must have bitvector sort.");`
	`88`	`+ validate_bit_vector_sorts(left, right);`
`74`	`89`	`// The below invariant is based on the smtlib standard.`
`75`	`90`	`// See http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV`
`76`	`91`	`INVARIANT(`
`77`		`- left_sort->bit_width() == right_sort->bit_width(),`
	`92`	`+ left.get_sort() == right.get_sort(),`
`78`	`93`	`"Left and right operands must have the same bit width.");`
`79`	`94`	`}`
`80`	`95`
`@@ -92,8 +107,7 @@ smt_sortt smt_bit_vector_theoryt::nott::return_sort(const smt_termt &operand)`
`92`	`107`
`93`	`108`	`void smt_bit_vector_theoryt::nott::validate(const smt_termt &operand)`
`94`	`109`	`{`
`95`		`- const auto operand_sort = operand.get_sort().cast<smt_bit_vector_sortt>();`
`96`		`- INVARIANT(operand_sort, "The operand is expected to have a bit-vector sort.");`
	`110`	`+ validate_bit_vector_sort(operand);`
`97`	`111`	`}`
`98`	`112`
`99`	`113`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nott>`
`@@ -115,7 +129,7 @@ void smt_bit_vector_theoryt::andt::validate(`
`115`	`129`	`const smt_termt &lhs,`
`116`	`130`	`const smt_termt &rhs)`
`117`	`131`	`{`
`118`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`132`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`119`	`133`	`}`
`120`	`134`
`121`	`135`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::andt>`
`@@ -137,7 +151,7 @@ void smt_bit_vector_theoryt::ort::validate(`
`137`	`151`	`const smt_termt &lhs,`
`138`	`152`	`const smt_termt &rhs)`
`139`	`153`	`{`
`140`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`154`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`141`	`155`	`}`
`142`	`156`
`143`	`157`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::ort>`
`@@ -159,7 +173,7 @@ void smt_bit_vector_theoryt::nandt::validate(`
`159`	`173`	`const smt_termt &lhs,`
`160`	`174`	`const smt_termt &rhs)`
`161`	`175`	`{`
`162`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`176`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`163`	`177`	`}`
`164`	`178`
`165`	`179`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nandt>`
`@@ -181,7 +195,7 @@ void smt_bit_vector_theoryt::nort::validate(`
`181`	`195`	`const smt_termt &lhs,`
`182`	`196`	`const smt_termt &rhs)`
`183`	`197`	`{`
`184`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`198`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`185`	`199`	`}`
`186`	`200`
`187`	`201`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nort>`
`@@ -203,7 +217,7 @@ void smt_bit_vector_theoryt::xort::validate(`
`203`	`217`	`const smt_termt &lhs,`
`204`	`218`	`const smt_termt &rhs)`
`205`	`219`	`{`
`206`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`220`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`207`	`221`	`}`
`208`	`222`
`209`	`223`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::xort>`
`@@ -225,7 +239,7 @@ void smt_bit_vector_theoryt::xnort::validate(`
`225`	`239`	`const smt_termt &lhs,`
`226`	`240`	`const smt_termt &rhs)`
`227`	`241`	`{`
`228`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`242`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`229`	`243`	`}`
`230`	`244`
`231`	`245`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::xnort>`
`@@ -249,7 +263,7 @@ void smt_bit_vector_theoryt::unsigned_less_thant::validate(`
`249`	`263`	`const smt_termt &lhs,`
`250`	`264`	`const smt_termt &rhs)`
`251`	`265`	`{`
`252`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`266`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`253`	`267`	`}`
`254`	`268`
`255`	`269`	`const smt_function_application_termt::factoryt<`
`@@ -272,7 +286,7 @@ void smt_bit_vector_theoryt::unsigned_less_than_or_equalt::validate(`
`272`	`286`	`const smt_termt &lhs,`
`273`	`287`	`const smt_termt &rhs)`
`274`	`288`	`{`
`275`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`289`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`276`	`290`	`}`
`277`	`291`
`278`	`292`	`const smt_function_application_termt::factoryt<`
`@@ -295,7 +309,7 @@ void smt_bit_vector_theoryt::unsigned_greater_thant::validate(`
`295`	`309`	`const smt_termt &lhs,`
`296`	`310`	`const smt_termt &rhs)`
`297`	`311`	`{`
`298`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`312`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`299`	`313`	`}`
`300`	`314`
`301`	`315`	`const smt_function_application_termt::factoryt<`
`@@ -319,7 +333,7 @@ void smt_bit_vector_theoryt::unsigned_greater_than_or_equalt::validate(`
`319`	`333`	`const smt_termt &lhs,`
`320`	`334`	`const smt_termt &rhs)`
`321`	`335`	`{`
`322`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`336`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`323`	`337`	`}`
`324`	`338`
`325`	`339`	`const smt_function_application_termt::factoryt<`
`@@ -342,7 +356,7 @@ void smt_bit_vector_theoryt::signed_less_thant::validate(`
`342`	`356`	`const smt_termt &lhs,`
`343`	`357`	`const smt_termt &rhs)`
`344`	`358`	`{`
`345`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`359`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`346`	`360`	`}`
`347`	`361`
`348`	`362`	`const smt_function_application_termt::factoryt<`
`@@ -365,7 +379,7 @@ void smt_bit_vector_theoryt::signed_less_than_or_equalt::validate(`
`365`	`379`	`const smt_termt &lhs,`
`366`	`380`	`const smt_termt &rhs)`
`367`	`381`	`{`
`368`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`382`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`369`	`383`	`}`
`370`	`384`
`371`	`385`	`const smt_function_application_termt::factoryt<`
`@@ -388,7 +402,7 @@ void smt_bit_vector_theoryt::signed_greater_thant::validate(`
`388`	`402`	`const smt_termt &lhs,`
`389`	`403`	`const smt_termt &rhs)`
`390`	`404`	`{`
`391`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`405`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`392`	`406`	`}`
`393`	`407`
`394`	`408`	`const smt_function_application_termt::factoryt<`
`@@ -411,7 +425,7 @@ void smt_bit_vector_theoryt::signed_greater_than_or_equalt::validate(`
`411`	`425`	`const smt_termt &lhs,`
`412`	`426`	`const smt_termt &rhs)`
`413`	`427`	`{`
`414`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`428`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`415`	`429`	`}`
`416`	`430`
`417`	`431`	`const smt_function_application_termt::factoryt<`
`@@ -434,7 +448,7 @@ void smt_bit_vector_theoryt::addt::validate(`
`434`	`448`	`const smt_termt &lhs,`
`435`	`449`	`const smt_termt &rhs)`
`436`	`450`	`{`
`437`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`451`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`438`	`452`	`}`
`439`	`453`
`440`	`454`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::addt>`
`@@ -456,7 +470,7 @@ void smt_bit_vector_theoryt::subtractt::validate(`
`456`	`470`	`const smt_termt &lhs,`
`457`	`471`	`const smt_termt &rhs)`
`458`	`472`	`{`
`459`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`473`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`460`	`474`	`}`
`461`	`475`
`462`	`476`	`const smt_function_application_termt::factoryt<`
`@@ -479,7 +493,7 @@ void smt_bit_vector_theoryt::multiplyt::validate(`
`479`	`493`	`const smt_termt &lhs,`
`480`	`494`	`const smt_termt &rhs)`
`481`	`495`	`{`
`482`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`496`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`483`	`497`	`}`
`484`	`498`
`485`	`499`	`const smt_function_application_termt::factoryt<`
`@@ -502,7 +516,7 @@ void smt_bit_vector_theoryt::unsigned_dividet::validate(`
`502`	`516`	`const smt_termt &lhs,`
`503`	`517`	`const smt_termt &rhs)`
`504`	`518`	`{`
`505`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`519`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`506`	`520`	`}`
`507`	`521`
`508`	`522`	`const smt_function_application_termt::factoryt<`
`@@ -525,7 +539,7 @@ void smt_bit_vector_theoryt::signed_dividet::validate(`
`525`	`539`	`const smt_termt &lhs,`
`526`	`540`	`const smt_termt &rhs)`
`527`	`541`	`{`
`528`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`542`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`529`	`543`	`}`
`530`	`544`
`531`	`545`	`const smt_function_application_termt::factoryt<`
`@@ -548,7 +562,7 @@ void smt_bit_vector_theoryt::unsigned_remaindert::validate(`
`548`	`562`	`const smt_termt &lhs,`
`549`	`563`	`const smt_termt &rhs)`
`550`	`564`	`{`
`551`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`565`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`552`	`566`	`}`
`553`	`567`
`554`	`568`	`const smt_function_application_termt::factoryt<`
`@@ -571,7 +585,7 @@ void smt_bit_vector_theoryt::signed_remaindert::validate(`
`571`	`585`	`const smt_termt &lhs,`
`572`	`586`	`const smt_termt &rhs)`
`573`	`587`	`{`
`574`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`588`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`575`	`589`	`}`
`576`	`590`
`577`	`591`	`const smt_function_application_termt::factoryt<`
`@@ -590,8 +604,7 @@ smt_sortt smt_bit_vector_theoryt::negatet::return_sort(const smt_termt &operand)`
`590`	`604`
`591`	`605`	`void smt_bit_vector_theoryt::negatet::validate(const smt_termt &operand)`
`592`	`606`	`{`
`593`		`- const auto operand_sort = operand.get_sort().cast<smt_bit_vector_sortt>();`
`594`		`- INVARIANT(operand_sort, "The operand is expected to have a bit-vector sort.");`
	`607`	`+ validate_bit_vector_sort(operand);`
`595`	`608`	`}`
`596`	`609`
`597`	`610`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::negatet>`
`@@ -613,7 +626,7 @@ void smt_bit_vector_theoryt::shift_leftt::validate(`
`613`	`626`	`const smt_termt &lhs,`
`614`	`627`	`const smt_termt &rhs)`
`615`	`628`	`{`
`616`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`629`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`617`	`630`	`}`
`618`	`631`
`619`	`632`	`const smt_function_application_termt::factoryt<`
`@@ -636,7 +649,7 @@ void smt_bit_vector_theoryt::logical_shift_rightt::validate(`
`636`	`649`	`const smt_termt &lhs,`
`637`	`650`	`const smt_termt &rhs)`
`638`	`651`	`{`
`639`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`652`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`640`	`653`	`}`
`641`	`654`
`642`	`655`	`const smt_function_application_termt::factoryt<`
`@@ -659,7 +672,7 @@ void smt_bit_vector_theoryt::arithmetic_shift_rightt::validate(`
`659`	`672`	`const smt_termt &lhs,`
`660`	`673`	`const smt_termt &rhs)`
`661`	`674`	`{`
`662`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`675`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`663`	`676`	`}`
`664`	`677`
`665`	`678`	`const smt_function_application_termt::factoryt<`