fix: pointer handling in solvers

metametamoon · metametamoon · commit f21b11ee90d4 · 2025-07-24T16:01:13.000+03:00
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
@@ -658,7 +658,7 @@ MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out) {
   switch (e->getKind()) {
   case Expr::Pointer:
   case Expr::ConstantPointer: {
-    assert(0 && "unreachable");
+    return constructActual(e->getValue(), width_out);
   }
 
   case Expr::Constant: {
diff --git a/lib/Solver/Z3CoreBuilder.cpp b/lib/Solver/Z3CoreBuilder.cpp
@@ -206,7 +206,7 @@ Z3ASTHandle Z3CoreBuilder::constructActual(ref<Expr> e, int *width_out) {
   switch (e->getKind()) {
   case Expr::Pointer:
   case Expr::ConstantPointer: {
-    assert(0 && "unreachable");
+    return constructActual(e->getValue(), width_out);
   }
 
   case Expr::Constant: {

Original file line number	Diff line number	Diff line change
`@@ -658,7 +658,7 @@ MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out) {`
`658`	`658`	`switch (e->getKind()) {`
`659`	`659`	`case Expr::Pointer:`
`660`	`660`	`case Expr::ConstantPointer: {`
`661`		`- assert(0 && "unreachable");`
	`661`	`+ return constructActual(e->getValue(), width_out);`
`662`	`662`	`}`
`663`	`663`
`664`	`664`	`case Expr::Constant: {`
Original file line number	Diff line number	Diff line change
`@@ -206,7 +206,7 @@ Z3ASTHandle Z3CoreBuilder::constructActual(ref<Expr> e, int *width_out) {`
`206`	`206`	`switch (e->getKind()) {`
`207`	`207`	`case Expr::Pointer:`
`208`	`208`	`case Expr::ConstantPointer: {`
`209`		`- assert(0 && "unreachable");`
	`209`	`+ return constructActual(e->getValue(), width_out);`
`210`	`210`	`}`
`211`	`211`
`212`	`212`	`case Expr::Constant: {`