Refactor to deduplicate shared bit vector validation code

thomasspriggs · thomasspriggs · commit 3ae261e9e7d5 · 2022-02-14T16:05:21.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,28 @@ 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_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 +77,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 +102,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("The", operand);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nott>
@@ -115,7 +124,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 +146,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 +168,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 +190,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 +212,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 +234,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 +258,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 +281,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 +304,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 +328,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 +351,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 +374,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 +397,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 +420,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 +443,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 +465,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 +488,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 +511,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 +534,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 +557,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 +580,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 +599,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("The", operand);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::negatet>
@@ -613,7 +621,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 +644,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 +667,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,28 @@ 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`
	`33`	`+validate_bit_vector_sorts(const smt_termt &lhs, const smt_termt &rhs)`
	`34`	`+{`
	`35`	`+ validate_bit_vector_sort("Left ", lhs);`
	`36`	`+ validate_bit_vector_sort("Right ", rhs);`
	`37`	`+}`
	`38`	`+`
`22`	`39`	`void smt_bit_vector_theoryt::concatt::validate(`
`23`	`40`	`const smt_termt &lhs,`
`24`	`41`	`const smt_termt &rhs)`
`25`	`42`	`{`
`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.");`
	`43`	`+ validate_bit_vector_sorts(lhs, rhs);`
`30`	`44`	`}`
`31`	`45`
`32`	`46`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::concatt>`
`@@ -63,18 +77,14 @@ smt_bit_vector_theoryt::extract(std::size_t i, std::size_t j)`
`63`	`77`	`return smt_function_application_termt::factoryt<extractt>(i, j);`
`64`	`78`	`}`
`65`	`79`
`66`		`-static void validate_bit_vector_operator_arguments(`
`67`		`- const smt_termt &left,`
`68`		`- const smt_termt &right)`
	`80`	`+static void`
	`81`	`+validate_matched_bit_vector_sorts(const smt_termt &left, const smt_termt &right)`
`69`	`82`	`{`
`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.");`
	`83`	`+ validate_bit_vector_sorts(left, right);`
`74`	`84`	`// The below invariant is based on the smtlib standard.`
`75`	`85`	`// See http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV`
`76`	`86`	`INVARIANT(`
`77`		`- left_sort->bit_width() == right_sort->bit_width(),`
	`87`	`+ left.get_sort() == right.get_sort(),`
`78`	`88`	`"Left and right operands must have the same bit width.");`
`79`	`89`	`}`
`80`	`90`
`@@ -92,8 +102,7 @@ smt_sortt smt_bit_vector_theoryt::nott::return_sort(const smt_termt &operand)`
`92`	`102`
`93`	`103`	`void smt_bit_vector_theoryt::nott::validate(const smt_termt &operand)`
`94`	`104`	`{`
`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.");`
	`105`	`+ validate_bit_vector_sort("The", operand);`
`97`	`106`	`}`
`98`	`107`
`99`	`108`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nott>`
`@@ -115,7 +124,7 @@ void smt_bit_vector_theoryt::andt::validate(`
`115`	`124`	`const smt_termt &lhs,`
`116`	`125`	`const smt_termt &rhs)`
`117`	`126`	`{`
`118`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`127`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`119`	`128`	`}`
`120`	`129`
`121`	`130`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::andt>`
`@@ -137,7 +146,7 @@ void smt_bit_vector_theoryt::ort::validate(`
`137`	`146`	`const smt_termt &lhs,`
`138`	`147`	`const smt_termt &rhs)`
`139`	`148`	`{`
`140`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`149`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`141`	`150`	`}`
`142`	`151`
`143`	`152`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::ort>`
`@@ -159,7 +168,7 @@ void smt_bit_vector_theoryt::nandt::validate(`
`159`	`168`	`const smt_termt &lhs,`
`160`	`169`	`const smt_termt &rhs)`
`161`	`170`	`{`
`162`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`171`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`163`	`172`	`}`
`164`	`173`
`165`	`174`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nandt>`
`@@ -181,7 +190,7 @@ void smt_bit_vector_theoryt::nort::validate(`
`181`	`190`	`const smt_termt &lhs,`
`182`	`191`	`const smt_termt &rhs)`
`183`	`192`	`{`
`184`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`193`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`185`	`194`	`}`
`186`	`195`
`187`	`196`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nort>`
`@@ -203,7 +212,7 @@ void smt_bit_vector_theoryt::xort::validate(`
`203`	`212`	`const smt_termt &lhs,`
`204`	`213`	`const smt_termt &rhs)`
`205`	`214`	`{`
`206`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`215`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`207`	`216`	`}`
`208`	`217`
`209`	`218`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::xort>`
`@@ -225,7 +234,7 @@ void smt_bit_vector_theoryt::xnort::validate(`
`225`	`234`	`const smt_termt &lhs,`
`226`	`235`	`const smt_termt &rhs)`
`227`	`236`	`{`
`228`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`237`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`229`	`238`	`}`
`230`	`239`
`231`	`240`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::xnort>`
`@@ -249,7 +258,7 @@ void smt_bit_vector_theoryt::unsigned_less_thant::validate(`
`249`	`258`	`const smt_termt &lhs,`
`250`	`259`	`const smt_termt &rhs)`
`251`	`260`	`{`
`252`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`261`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`253`	`262`	`}`
`254`	`263`
`255`	`264`	`const smt_function_application_termt::factoryt<`
`@@ -272,7 +281,7 @@ void smt_bit_vector_theoryt::unsigned_less_than_or_equalt::validate(`
`272`	`281`	`const smt_termt &lhs,`
`273`	`282`	`const smt_termt &rhs)`
`274`	`283`	`{`
`275`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`284`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`276`	`285`	`}`
`277`	`286`
`278`	`287`	`const smt_function_application_termt::factoryt<`
`@@ -295,7 +304,7 @@ void smt_bit_vector_theoryt::unsigned_greater_thant::validate(`
`295`	`304`	`const smt_termt &lhs,`
`296`	`305`	`const smt_termt &rhs)`
`297`	`306`	`{`
`298`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`307`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`299`	`308`	`}`
`300`	`309`
`301`	`310`	`const smt_function_application_termt::factoryt<`
`@@ -319,7 +328,7 @@ void smt_bit_vector_theoryt::unsigned_greater_than_or_equalt::validate(`
`319`	`328`	`const smt_termt &lhs,`
`320`	`329`	`const smt_termt &rhs)`
`321`	`330`	`{`
`322`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`331`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`323`	`332`	`}`
`324`	`333`
`325`	`334`	`const smt_function_application_termt::factoryt<`
`@@ -342,7 +351,7 @@ void smt_bit_vector_theoryt::signed_less_thant::validate(`
`342`	`351`	`const smt_termt &lhs,`
`343`	`352`	`const smt_termt &rhs)`
`344`	`353`	`{`
`345`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`354`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`346`	`355`	`}`
`347`	`356`
`348`	`357`	`const smt_function_application_termt::factoryt<`
`@@ -365,7 +374,7 @@ void smt_bit_vector_theoryt::signed_less_than_or_equalt::validate(`
`365`	`374`	`const smt_termt &lhs,`
`366`	`375`	`const smt_termt &rhs)`
`367`	`376`	`{`
`368`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`377`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`369`	`378`	`}`
`370`	`379`
`371`	`380`	`const smt_function_application_termt::factoryt<`
`@@ -388,7 +397,7 @@ void smt_bit_vector_theoryt::signed_greater_thant::validate(`
`388`	`397`	`const smt_termt &lhs,`
`389`	`398`	`const smt_termt &rhs)`
`390`	`399`	`{`
`391`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`400`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`392`	`401`	`}`
`393`	`402`
`394`	`403`	`const smt_function_application_termt::factoryt<`
`@@ -411,7 +420,7 @@ void smt_bit_vector_theoryt::signed_greater_than_or_equalt::validate(`
`411`	`420`	`const smt_termt &lhs,`
`412`	`421`	`const smt_termt &rhs)`
`413`	`422`	`{`
`414`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`423`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`415`	`424`	`}`
`416`	`425`
`417`	`426`	`const smt_function_application_termt::factoryt<`
`@@ -434,7 +443,7 @@ void smt_bit_vector_theoryt::addt::validate(`
`434`	`443`	`const smt_termt &lhs,`
`435`	`444`	`const smt_termt &rhs)`
`436`	`445`	`{`
`437`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`446`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`438`	`447`	`}`
`439`	`448`
`440`	`449`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::addt>`
`@@ -456,7 +465,7 @@ void smt_bit_vector_theoryt::subtractt::validate(`
`456`	`465`	`const smt_termt &lhs,`
`457`	`466`	`const smt_termt &rhs)`
`458`	`467`	`{`
`459`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`468`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`460`	`469`	`}`
`461`	`470`
`462`	`471`	`const smt_function_application_termt::factoryt<`
`@@ -479,7 +488,7 @@ void smt_bit_vector_theoryt::multiplyt::validate(`
`479`	`488`	`const smt_termt &lhs,`
`480`	`489`	`const smt_termt &rhs)`
`481`	`490`	`{`
`482`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`491`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`483`	`492`	`}`
`484`	`493`
`485`	`494`	`const smt_function_application_termt::factoryt<`
`@@ -502,7 +511,7 @@ void smt_bit_vector_theoryt::unsigned_dividet::validate(`
`502`	`511`	`const smt_termt &lhs,`
`503`	`512`	`const smt_termt &rhs)`
`504`	`513`	`{`
`505`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`514`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`506`	`515`	`}`
`507`	`516`
`508`	`517`	`const smt_function_application_termt::factoryt<`
`@@ -525,7 +534,7 @@ void smt_bit_vector_theoryt::signed_dividet::validate(`
`525`	`534`	`const smt_termt &lhs,`
`526`	`535`	`const smt_termt &rhs)`
`527`	`536`	`{`
`528`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`537`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`529`	`538`	`}`
`530`	`539`
`531`	`540`	`const smt_function_application_termt::factoryt<`
`@@ -548,7 +557,7 @@ void smt_bit_vector_theoryt::unsigned_remaindert::validate(`
`548`	`557`	`const smt_termt &lhs,`
`549`	`558`	`const smt_termt &rhs)`
`550`	`559`	`{`
`551`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`560`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`552`	`561`	`}`
`553`	`562`
`554`	`563`	`const smt_function_application_termt::factoryt<`
`@@ -571,7 +580,7 @@ void smt_bit_vector_theoryt::signed_remaindert::validate(`
`571`	`580`	`const smt_termt &lhs,`
`572`	`581`	`const smt_termt &rhs)`
`573`	`582`	`{`
`574`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`583`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`575`	`584`	`}`
`576`	`585`
`577`	`586`	`const smt_function_application_termt::factoryt<`
`@@ -590,8 +599,7 @@ smt_sortt smt_bit_vector_theoryt::negatet::return_sort(const smt_termt &operand)`
`590`	`599`
`591`	`600`	`void smt_bit_vector_theoryt::negatet::validate(const smt_termt &operand)`
`592`	`601`	`{`
`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.");`
	`602`	`+ validate_bit_vector_sort("The", operand);`
`595`	`603`	`}`
`596`	`604`
`597`	`605`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::negatet>`
`@@ -613,7 +621,7 @@ void smt_bit_vector_theoryt::shift_leftt::validate(`
`613`	`621`	`const smt_termt &lhs,`
`614`	`622`	`const smt_termt &rhs)`
`615`	`623`	`{`
`616`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`624`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`617`	`625`	`}`
`618`	`626`
`619`	`627`	`const smt_function_application_termt::factoryt<`
`@@ -636,7 +644,7 @@ void smt_bit_vector_theoryt::logical_shift_rightt::validate(`
`636`	`644`	`const smt_termt &lhs,`
`637`	`645`	`const smt_termt &rhs)`
`638`	`646`	`{`
`639`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`647`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`640`	`648`	`}`
`641`	`649`
`642`	`650`	`const smt_function_application_termt::factoryt<`
`@@ -659,7 +667,7 @@ void smt_bit_vector_theoryt::arithmetic_shift_rightt::validate(`
`659`	`667`	`const smt_termt &lhs,`
`660`	`668`	`const smt_termt &rhs)`
`661`	`669`	`{`
`662`		`- validate_bit_vector_operator_arguments(lhs, rhs);`
	`670`	`+ validate_matched_bit_vector_sorts(lhs, rhs);`
`663`	`671`	`}`
`664`	`672`
`665`	`673`	`const smt_function_application_termt::factoryt<`