Refactor to deduplicate shared bit vector validation code

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